diff options
| -rw-r--r-- | camlp4/boot/Makefile | 24 |
1 files changed, 0 insertions, 24 deletions
diff --git a/camlp4/boot/Makefile b/camlp4/boot/Makefile deleted file mode 100644 index b6a146310..000000000 --- a/camlp4/boot/Makefile +++ /dev/null @@ -1,24 +0,0 @@ - - -MAX_SAVE = 10 - -backup: - cp camlp4boot camlp4boot.save.0 - set -e; for i in camlp4boot.save.*; do \ - mv $$i camlp4boot.evas.$$((`echo $$i | sed -e 's/.*\.save\.\([0-9][0-9]*\)/\1/'` + 1)); \ - done - set -e; for i in camlp4boot.evas.*; do mv $$i $${i/.evas./.save.}; done - rm -f camlp4boot.save.$(MAX_SAVE) - -restore: - set -e; for i in camlp4boot.save.*; do \ - mv $$i camlp4boot.evas.$$((`echo $$i | sed -e 's/.*\.save\.\([0-9][0-9]*\)/\1/'` - 1)); \ - done - set -e; for i in camlp4boot.evas.*; do mv $$i $${i/.evas./.save.}; done - mv camlp4boot.save.0 camlp4boot - -boot-clean: - rm -f camlp4boot.save.* camlp4boot.evas.* - -maintainer-clean: - rm -f camlp4boot |