aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile3
1 files changed, 3 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index c976f4367..4e0539beb 100644
--- a/Makefile
+++ b/Makefile
@@ -106,6 +106,9 @@ $(DISPLAY_JAVA_VO:.vo=.log) : %JavaDisplay.log : %.vo %JavaDisplay.v src/Compile
$(SHOW)"COQC $*JavaDisplay > $@"
$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $*JavaDisplay.v > $@.tmp && mv -f $@.tmp $@
+src/Specific/x25519_c64.c: src/Specific/x25519_c64.c.sh src/Specific/IntegrationTestMulDisplay.log
+ bash src/Specific/x25519_c64.c.sh > src/Specific/x25519_c64.c
+
clean::
rm -f Makefile.coq