Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Janno
iris-coq
Commits
46cb853d
Commit
46cb853d
authored
Jun 26, 2018
by
Ralf Jung
Browse files
MAKE_REF overwrites COQ_BROKEN
parent
52c96f45
Changes
1
Hide whitespace changes
Inline
Side-by-side
Makefile.coq.local
View file @
46cb853d
...
...
@@ -21,14 +21,15 @@ tests/.coqdeps.d: $(TESTFILES)
-include
tests/.coqdeps.d
$(TESTFILES
:
.v=.vo): %.vo: %.v $(if $(MAKE_REF)
,,
%.ref)
$(SHOW)
$(
if
$(
COQ_BROKEN
)
,COQTEST
[
igno
re],
$(
if
$(
MAKE_REF
)
,COQTEST
[
re
f
],COQTEST
))
$<
$(SHOW)
$(
if
$(
MAKE_REF
)
,COQTEST
[
re
f
],
$(
if
$(
COQ_BROKEN
)
,COQTEST
[
igno
re
d
],COQTEST
))
$<
$(HIDE)TEST
=
"
$
$(
basename
-s .v
$<
)
"
&&
\
TMPFILE
=
"
$
$(mktemp)
"
&&
\
$(TIMER)
$(COQ_TEST)
$(TIMING_ARG)
$(COQFLAGS)
$(COQLIBS)
-load-vernac-source
$<
$(TIMING_EXTRA)
>
"
$$
TMPFILE"
&&
\
(
$(REF_FILTER)
<
"
$$
TMPFILE"
>
"
$$
TMPFILE.filtered"
||
true
)
&&
\
$(
if
$(COQ_BROKEN)
,
true
,
\
$(
if
$(MAKE_REF)
,
\
mv
"
$$
TMPFILE.filtered"
"tests/
$$
TEST.ref"
,
\
$(
if
$(MAKE_REF)
,
\
mv
"
$$
TMPFILE.filtered"
"tests/
$$
TEST.ref"
,
\
$(
if
$(COQ_BROKEN)
,
\
true
,
\
diff
-u
"tests/
$$
TEST.ref"
"
$$
TMPFILE.filtered"
\
)
\
)
&&
\
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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