diff -r 74c1b51c1cd9 -r 24dae6222579 etc/user-settings.sample
--- a/etc/user-settings.sample	Tue May 06 15:24:41 1997 +0200
+++ b/etc/user-settings.sample	Tue May 06 15:27:35 1997 +0200
@@ -15,7 +15,10 @@
 ### Heap files
 ###
 
+# Note: ML system identifier appended automatically!
+
 #ISABELLE_PATH=other-places-where-heaps-may-reside:$ISABELLE_PATH
+#ISABELLE_OUTPUT=somewhere-else
 
 #DEFAULT_LOGIC=ZF