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
---
 parsing/ppvernac.ml    | 4 ++--
 tools/beautify-archive | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)
 mode change 100644 => 100755 tools/beautify-archive

diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index b1ba16b5cf..849f67fe68 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -414,8 +414,8 @@ let pr_grammar_tactic_rule n (_,pil,t) =
 
 let pr_statement head (id,(bl,c,guard)) =
   assert (id<>None);
-  hov 0
-    (head ++ pr_lident (Option.get id) ++ spc() ++
+  hov 1
+    (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++
     (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
     pr_opt (pr_guard_annot bl) guard ++
     str":" ++ pr_spc_lconstr c)
diff --git a/tools/beautify-archive b/tools/beautify-archive
old mode 100644
new mode 100755
index aac6f3e0e5..ccfeb3dbaa
--- 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