Skip to content

Commit 2802c35

Browse files
adomanidagurtomas
authored andcommitted
fix: add space in no_lost_declarations regex (#14080)
As [reported](#14048 (comment)) and [requested](#14048 (comment)) by Yael! I think that this change is an improvement, but I would be happier if there was a consensus that the `def`, `theorem`, `structure`,... keywords are followed by a space and not a line break before their identifier.
1 parent ada0160 commit 2802c35

File tree

1 file changed

+4
-4
lines changed

1 file changed

+4
-4
lines changed

scripts/no_lost_declarations.sh

+4-4
Original file line numberDiff line numberDiff line change
@@ -18,9 +18,9 @@ else
1818
fi |
1919
## purge `@[...]`, to attempt to catch declaration names
2020
sed 's=@\[[^]]*\] ==; s=noncomputable ==; s=nonrec ==; s=protected ==' |
21-
## extract lines that begin with '[+-]' followed by the input `theorem` or `lemma`
22-
## in the `git diff`
23-
awk -v regex="^[+-]${begs}" 'BEGIN{ paired=0; added=0; removed=0 }
21+
## extract lines that begin with '[+-]' followed by the input `theorem`, `lemma`,...
22+
## and then a space in the `git diff`
23+
awk -v regex="^[+-]${begs} " 'BEGIN{ paired=0; added=0; removed=0 }
2424
/^--- a\// { minusFile=$2 } ## the path to the old file
2525
/^\+\+\+ b\// { plusFile=$2 } ## the path to the new file
2626
($0 ~ regex){
@@ -132,5 +132,5 @@ instance (priority := high) {to be a nameless} instance :=
132132
def testingLongDiff1 im a def
133133
def testingLongDiff2 im a def
134134
def testingLongDiff3 im a def
135-
def testingLongDiff4 im a def
135+
@[trying to fool you] instance. the messing dot
136136
ReferenceTest

0 commit comments

Comments
 (0)