aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-04-15 15:04:54 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2018-04-18 20:38:49 -0400
commit7bdab68b6e531e0260d199eb96af243b085bdc1a (patch)
treef4c96d80c0bcd88b83b93987cc01e5755c70b7ea /Makefile
parentdf32529c2df958d9059d16c5af9ff614c790546e (diff)
Add COQLIBS to display targets
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index f90413e96..b8989ace4 100644
--- a/Makefile
+++ b/Makefile
@@ -226,7 +226,7 @@ $(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) $< > $@.tmp
+ $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > $@.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))