From b33c18ba8edc25c7f4b0be62db4e845dc8693a2f Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 16 Nov 2011 08:46:27 +0000 Subject: 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 --- tools/beautify-archive | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) mode change 100644 => 100755 tools/beautify-archive (limited to 'tools/beautify-archive') diff --git a/tools/beautify-archive b/tools/beautify-archive old mode 100644 new mode 100755 index aac6f3e0e..ccfeb3dba --- 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'"' -- cgit v1.2.3