diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:04 +0200 |
| commit | ada0e568ed7d5d25ab6bff4eae72afc30c3f675f (patch) | |
| tree | e9a1fff9f8b89056f321244487cd6f91e7b56769 | |
| parent | 200eb1f9494048ba4fb66af28a34d878dcf31cac (diff) | |
Revert "Adding a target check-beautify for testing reparsability of"
This reverts commit 973b6c69f0861c113f7bd5b94604d2497520a334.
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | Makefile.build | 34 |
2 files changed, 1 insertions, 35 deletions
diff --git a/.gitignore b/.gitignore index 2e5c74c3d..b50bca3cf 100644 --- a/.gitignore +++ b/.gitignore @@ -38,8 +38,6 @@ *.v.html *.stamp *.native -*.beautified -*.backup revision TAGS .DS_Store diff --git a/Makefile.build b/Makefile.build index fb6bfa87f..6a25eda75 100644 --- a/Makefile.build +++ b/Makefile.build @@ -498,25 +498,6 @@ test-suite: world $(ALLSTDLIB).v $(MAKE) $(MAKE_TSOPTS) all $(MAKE) $(MAKE_TSOPTS) report -BEAUTIFIED=$(THEORIESVO) -TOBEAUTIFY=$(BEAUTIFIED:.vo=.v.beautified) - -check-beautify: $(TOBEAUTIFY) - @echo Upgrading with beautified files - $(HIDE)for i in $(TOBEAUTIFY);\ - do j=`dirname $$i`/`basename $$i .v.beautified`.v;\ - mv -f $$j $$j.backup;\ - if [ $$i -nt $$j ]; then mv -f $$i $$j; fi;\ - rm -f "$$j"o;\ - done - @echo Recompiling beautified files - $(HIDE)$(MAKE) $(BEAUTIFIED) - @echo Restoring initial files - $(HIDE)for i in $(TOBEAUTIFY);\ - do j=`dirname $$i`/`basename $$i .v.beautified`.v;\ - mv -f $$j.backup $$j;\ - done; - ################################################################## # partial targets: 1) core ML parts ################################################################## @@ -1129,24 +1110,11 @@ theories/Init/%.v.beautified: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/ $(HIDE)rm -f theories/Init/$*.glob $(HIDE)$(BOOTCOQC) $< -beautify -noinit -R theories Coq -%.v.beautified: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d +%.v.beautified: %.v | %.v.d $(SHOW)'COQC -beautify $<' $(HIDE)rm -f $*.glob $(HIDE)$(BOOTCOQC) $< -beautify -theories/Init/%.v.backup: theories/Init/%.v.beautified $(VO_TOOLS_DEP) | theories/Init/%.v.d - $(SHOW)'COQC -noinit $<' - mv -f theories/Init/$*.v theories/Init/$*.v.backup - mv -f theories/Init/$*.v.beautified theories/Init/$*.v - rm -f theories/Init/$*.vo - $(BOOTCOQC) theories/Init/$* -noinit -R theories Coq - -%.v.backup: %.v.beautified theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d - $(SHOW)'COQC $<.v.beautified' - $(HIDE)mv -f $*.v $*.v.backup - $(HIDE)mv -f $*.v.beautified $*.v - $(HIDE)$(BOOTCOQC) $* - ########################################################################### # this sets up developper supporting stuff ########################################################################### |