diff options
| -rw-r--r-- | camlp4/boot/Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/camlp4/boot/Makefile b/camlp4/boot/Makefile index 1630917ec..d8624d43d 100644 --- a/camlp4/boot/Makefile +++ b/camlp4/boot/Makefile @@ -5,14 +5,14 @@ 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]\+\)/\1/'` + 1)); \ + 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]\+\)/\1/'` - 1)); \ + 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 |