lib/Tools/version

--- a/lib/Tools/version	Fri Aug 17 11:37:14 2012 +0200
+++ b/lib/Tools/version	Fri Aug 17 11:42:05 2012 +0200
@@ -60,7 +60,7 @@
   if [ -n "$ISABELLE_ID" ]; then
     echo "$ISABELLE_ID"
   else
-    ${HG:-hg} id --repository "$ISABELLE_HOME" --id 2>/dev/null || echo undefined
+    "${HG:-hg}" id --repository "$ISABELLE_HOME" --id 2>/dev/null || echo undefined
   fi
 else
   echo 'unidentified repository version'    # filled in automatically!