diff -r 0aadfaf8557a -r 508d2a233dbc lib/scripts/getsettings
--- 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