diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-16 08:46:27 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-16 08:46:27 +0000 |
| commit | b33c18ba8edc25c7f4b0be62db4e845dc8693a2f (patch) | |
| tree | 4953c33fc33986555e3b9b5a6f3a84df585bd32f /tools/beautify-archive | |
| parent | 2556a4bcfe9bbad8b3fe555997bb272102fec1dd (diff) | |
Fixing beautification of "thm_token" (missing space) + improvements.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14654 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/beautify-archive')
| -rwxr-xr-x[-rw-r--r--] | tools/beautify-archive | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/beautify-archive b/tools/beautify-archive index aac6f3e0e..ccfeb3dba 100644..100755 --- a/tools/beautify-archive +++ b/tools/beautify-archive @@ -47,6 +47,6 @@ for i in $vfiles; do mv -u -f $NEWARCHIVE/$i $i done echo -------- Beautification completed ------------------------------------- -echo Old files are in directory '"$OLDARCHIVE"' +echo Old files are in directory '"'$OLDARCHIVE'"' echo New files are in current directory -echo You can now remove the beautification directory '"$NEWARCHIVE"' +echo You can now remove the beautification directory '"'$NEWARCHIVE'"' |