lib/scripts/getsettings
changeset 2307 508d2a233dbc
parent 2299 ed9720047d53
child 2348 b51e104ecf40
--- a/lib/scripts/getsettings	Wed Dec 04 12:30:49 1996 +0100
+++ b/lib/scripts/getsettings	Wed Dec 04 13:05:47 1996 +0100
@@ -1,8 +1,8 @@
+#
+# $Id$
 #
 # getsettings - bash source script to augment current env
 #
-# $Id$
-#
 
 #value set by caller
 export ISABELLE_HOME