Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Tej Chajed
stdpp
Commits
183fdb94
Verified
Commit
183fdb94
authored
Nov 23, 2021
by
Tej Chajed
Browse files
Use GNU grep on macOS in coq-lint.sh
parent
9765b5fe
Pipeline
#57755
passed with stage
in 7 minutes and 18 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
coq-lint.sh
View file @
183fdb94
...
...
@@ -4,7 +4,13 @@ set -e
FILE
=
"
$1
"
if
egrep
-n
'^\s*((Existing\s+|Program\s+|Declare\s+|)Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope|Opaque|Transparent)\b'
"
$FILE
"
;
then
GREP
=
"grep"
# on macOS, use GNU grep if available
if
command
-v
ggrep &>/dev/null
;
then
GREP
=
ggrep
fi
if
$GREP
-E
-n
'^\s*((Existing\s+|Program\s+|Declare\s+|)Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope|Opaque|Transparent)\b'
"
$FILE
"
;
then
echo
"ERROR:
$FILE
contains 'Instance'/'Arguments'/'Hint' or another side-effect without locality (see above)."
echo
"Please add 'Global' or 'Local' as appropriate."
echo
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment