# HG changeset patch
# User huffman
# Date 1333120896 -7200
# Node ID ba37aaead15556d7f4424ec3bff09b22d5e96e45
# Parent  4f4d85c3516f1cf0a0e8f893d46bdb00d318113a# Parent  ca516aa5b6ce55f57d05c212de14ec784f58960a
merged

diff -r 4f4d85c3516f -r ba37aaead155 Admin/isatest/isatest-settings
--- a/Admin/isatest/isatest-settings	Fri Mar 30 16:44:23 2012 +0200
+++ b/Admin/isatest/isatest-settings	Fri Mar 30 17:21:36 2012 +0200
@@ -7,6 +7,8 @@
 # source bashrc, we're called by cron
 . ~/.bashrc
 
+export ISABELLE_JDK_HOME="$JAVA_HOME"
+
 # canoncical home for all platforms
 HOME=/home/isatest
 
diff -r 4f4d85c3516f -r ba37aaead155 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Fri Mar 30 16:44:23 2012 +0200
+++ b/src/HOL/Unix/Unix.thy	Fri Mar 30 17:21:36 2012 +0200
@@ -845,7 +845,7 @@
 
 
 
-definition invariant where 
+definition
   "invariant root path =
     (\<exists>att dir.
       access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>