diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-06 18:20:35 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-06 18:20:35 -0400 |
| commit | be79f23b1b0ba22d0063821d233ed86185b11ca6 (patch) | |
| tree | 86d7334c9f714fdeaac48981e953cf39e31fa672 /Makefile | |
| parent | eb6f1f415868acca3a0cdb3837b2871b0907fe5f (diff) | |
Clean up coq_makefile invocation
We don't need that part of the `sed` command anymore, now that we no
longer support 8.4.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -80,7 +80,7 @@ install-coqprime: Makefile.coq: Makefile _CoqProject $(SHOW)'COQ_MAKEFILE -f _CoqProject > $@' - $(HIDE)$(COQBIN)coq_makefile -f _CoqProject | sed s'|^\(-include.*\)$$|ifneq ($$(filter-out $(FAST_TARGETS),$$(MAKECMDGOALS)),)~\1~else~ifeq ($$(MAKECMDGOALS),)~\1~endif~endif|g' | tr '~' '\n' | sed s'/^clean:$$/clean::/g' | sed s'/^Makefile: /Makefile-old: /g' | sed s'/^printenv:$$/printenv::/g' > $@ + $(HIDE)$(COQBIN)coq_makefile -f _CoqProject | sed s'/^clean:$$/clean::/g' | sed s'/^Makefile: /Makefile-old: /g' | sed s'/^printenv:$$/printenv::/g' > $@ #$(DISPLAY_NON_JAVA_VO:.vo=.log) : %Display.log : %.vo %Display.v src/Reflection/Z/CNotations.vo # $(SHOW)"COQC $*Display > $@" |