aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorDavid Monniaux <David.Monniaux@univ-grenoble-alpes.fr>2022-02-02 15:53:13 +0100
committerDavid Monniaux <David.Monniaux@univ-grenoble-alpes.fr>2022-02-02 15:53:13 +0100
commit2b05d4e7657a0d838e1003ababf19dca43029b64 (patch)
tree98eb58baa84a149a38a6bead839248519cd32e6e /Makefile
parent657a8d362bfdfdcd362749f68ec2b661d166df0b (diff)
downloadcompcert-kvx-2b05d4e7657a0d838e1003ababf19dca43029b64.tar.gz
compcert-kvx-2b05d4e7657a0d838e1003ababf19dca43029b64.zip
attempts at dealing with gappa
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile9
1 files changed, 8 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 8b50375f..5ed2c580 100644
--- a/Makefile
+++ b/Makefile
@@ -77,7 +77,7 @@ COQCOPTS ?= \
cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality
-COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS)
+COQC=PATH=tools:$$PATH "$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS)
COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
COQDOC="$(COQBIN)coqdoc"
COQEXEC="$(COQBIN)coqtop" $(COQINCLUDES) -batch -load-vernac-source
@@ -297,6 +297,13 @@ else
ocamlc -o tools/modorder str.cma tools/modorder.ml
endif
+tools/gappa:
+ echo "#!/bin/sh" > $@
+ echo -n "exec " >> $@
+ which gappa | tr -d '\n' >> $@
+ echo ' -Eprecision=100 "$$@"' >> $@
+ chmod a+rx $@
+
latexdoc:
cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES)