diff -r ca186ebbd824 -r b1c6f4563df7 etc/user-settings.sample
--- a/etc/user-settings.sample	Sat Dec 20 11:39:34 2008 +0100
+++ b/etc/user-settings.sample	Sat Dec 20 11:55:34 2008 +0100
@@ -1,5 +1,4 @@
 # -*- shell-script -*-
-# $Id$
 #
 # Isabelle user settings sample -- for use in ~/.isabelle/etc/settings