diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-04-15 14:56:18 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-04-18 20:38:49 -0400 |
| commit | df32529c2df958d9059d16c5af9ff614c790546e (patch) | |
| tree | cb91e3acaae16cf4c35a85fe739df7a96ca89eb4 /Makefile | |
| parent | 476cf88ac2279956ca496a67902235a5d0704812 (diff) | |
Error if a display target fails
Because pipes eat error codes, we were previously succeeding when
display targets fail. This meant that we didn't catch
https://github.com/mit-plv/fiat-crypto/issues/344#issuecomment-381422896
on Travis. Now we will.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -226,7 +226,8 @@ $(DISPLAY_NON_JAVA_VO:.vo=.log) : %Display.log : %.vo src/Compilers/Z/CNotations $(DISPLAY_NON_JAVA_VO:.vo=.log) : %.log : %.v $(SHOW)'COQC $< > $@' - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $< | sed s'/\r\n/\n/g' > $@.tmp && mv -f $@.tmp $@ + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $< > $@.tmp + $(HIDE)sed s'/\r\n/\n/g' $@.tmp > $@ && rm -f $@.tmp DISPLAY_X25519_C64_VO := $(filter src/Specific/X25519/C64/%,$(DISPLAY_NON_JAVA_VO)) DISPLAY_X25519_C32_VO := $(filter src/Specific/X25519/C32/%,$(DISPLAY_NON_JAVA_VO)) |