diff options
| author | barras | 2001-06-13 08:45:04 +0000 |
|---|---|---|
| committer | barras | 2001-06-13 08:45:04 +0000 |
| commit | 560dd7089c3f5304db9596486ea423484f86c891 (patch) | |
| tree | 97f2a6f12092a8745ca9f75c3609241c88c3e0ae /tools | |
| parent | 3119ba6369bead12cae1fbcc26136561b744ea2e (diff) | |
plus besoin de separer les ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1786 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/translate_V6-3-1_to_V7-0 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tools/translate_V6-3-1_to_V7-0 b/tools/translate_V6-3-1_to_V7-0 index a89cced5c9..10e7f1403d 100755 --- a/tools/translate_V6-3-1_to_V7-0 +++ b/tools/translate_V6-3-1_to_V7-0 @@ -8,8 +8,7 @@ echo "- Various renamings of commands as described in document Changes.ps" for i in $* do sed -e "s/\.\([A-Z]\)/\. \1/g" -e "s/AddPath/Add LoadPath/g" \ - -e "s/~</~ </g" -e "s/|</| </g" -e "s/\([^ ]\)\?/\1 \?/g" \ - -e "s/\?\([^ ]\)/\? \1/g" \ + -e "s/~</~ </g" -e "s/|</| </g" \ -e "s/AddPath/Add LoadPath/g" -e "s/DelPath/Remove LoadPath/g" \ -e "s/AddRecPath/Add Rec LoadPath/g" \ -e "s/Implicit *Arguments *On/Set Implicit Arguments/g" \ |