aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-09 17:27:53 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-27 21:55:45 +0200
commitc2249c3b4c3387a3c8510e68fc447274d7299695 (patch)
treee9a1fff9f8b89056f321244487cd6f91e7b56769 /Makefile.build
parentf7ea0193c1aac918d8ed2df0d53df38dde5d1152 (diff)
Adding a target for beautification.
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build10
1 files changed, 10 insertions, 0 deletions
diff --git a/Makefile.build b/Makefile.build
index 190a62d00..6a25eda75 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -1105,6 +1105,16 @@ dev/%.mllib.d: $(D_DEPEND_BEFORE_SRC) dev/%.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLL
$(SHOW)'CCDEP $<'
$(HIDE)$(OCAMLC) -ccopt "-MM -MQ $@ -MQ $(<:.c=.o) -isystem $(CAMLHLIB)" $< $(TOTARGET)
+theories/Init/%.v.beautified: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/%.v.d
+ $(SHOW)'COQC -beautify -noinit $<'
+ $(HIDE)rm -f theories/Init/$*.glob
+ $(HIDE)$(BOOTCOQC) $< -beautify -noinit -R theories Coq
+
+%.v.beautified: %.v | %.v.d
+ $(SHOW)'COQC -beautify $<'
+ $(HIDE)rm -f $*.glob
+ $(HIDE)$(BOOTCOQC) $< -beautify
+
###########################################################################
# this sets up developper supporting stuff
###########################################################################