diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:02 +0200 |
| commit | 2f772c3347c45cb5173472924a69ab83dd9da626 (patch) | |
| tree | 2f083695ad7d49fff21a572fd4969a06d01fedcc | |
| parent | 1289b016fea5a54eb247cba1cac1fd9a19ee6d32 (diff) | |
Revert "Revert "Re-add -beautify by default.""
This reverts commit 67335c832a55cbd0ca559906bbe1af2485241353.
| -rw-r--r-- | Makefile.build | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build index b551242f6..3227d9e9e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -82,7 +82,7 @@ STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)" TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE) -BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile +BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -beautify -compile # The SHOW and HIDE variables control whether make will echo complete commands # or only abbreviated versions. @@ -502,7 +502,7 @@ BEAUTIFIED=$(THEORIESVO) $(PLUGINSVO) TOBEAUTIFY=$(BEAUTIFIED:.vo=.v.beautified) check-beautify: $(TOBEAUTIFY) - @echo Upgrading with beautified files + @echo Upgrading beautified files $(HIDE)for i in $(TOBEAUTIFY);\ do j=`dirname $$i`/`basename $$i .v.beautified`.v;\ mv -f $$j $$j.backup;\ |