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
18c2d6e8
Commit
18c2d6e8
authored
Oct 04, 2018
by
Ralf Jung
Browse files
UI tests actually work for current Coq
parent
a5f2f7bf
Changes
1
Hide whitespace changes
Inline
Side-by-side
Makefile.coq.local
View file @
18c2d6e8
...
...
@@ -8,7 +8,7 @@ test: $(TESTFILES:.v=.vo)
.PHONY
:
test
COQ_TEST
=
$(COQTOP)
$(COQDEBUG)
-batch
-test-mode
COQ_BROKEN
=
$(
shell
echo
"
$(COQ_VERSION)
"
| egrep
"^8
\.
9
\b
"
>
/dev/null
&&
echo
1
)
COQ_BROKEN
=
# Can't use pipes because that discards error codes and dash provides no way to control that.
# Also egrep errors if it doesn't match anything, we have to ignore that.
...
...
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