aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-12-25 14:13:45 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-12-25 14:13:45 +0000
commitc96e8baeb12706668ad1544f46b45088cc65ca2a (patch)
treeede1bfcc29bc180b97679309796062db9bafa1af /tools
parent2601b81a7f2fc5c829a56796e17e72331062202d (diff)
Traducteur automatique de scripts vernac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1198 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rwxr-xr-xtools/translate_V6-3-1_to_V7-014
1 files changed, 14 insertions, 0 deletions
diff --git a/tools/translate_V6-3-1_to_V7-0 b/tools/translate_V6-3-1_to_V7-0
new file mode 100755
index 000000000..4e49a9026
--- /dev/null
+++ b/tools/translate_V6-3-1_to_V7-0
@@ -0,0 +1,14 @@
+#! /bin/sh
+
+echo Insertion of a space after a dot not followed by a separator
+for i in $*
+ do sed -e "s/\.\([A-Z]\)/\. \1/g" -e "s/AddPath$i/Add LoadPath/g" > $i.tmp$$
+ if diff $i.tmp$$ $i > /dev/null
+ then
+ rm $i.tmp$$
+ else
+ echo Le fichier $i a été modifié
+ mv $i.tmp$$ $i
+ fi
+ done
+echo