# HG changeset patch
# User noschinl
# Date 1401971864 -7200
# Node ID 011955e7846bf2088eedbafbecba38f729f79cab
# Parent  276befcd90d9c691b5a7161f7fb80668a29ba259
mira: USER_HOME must exist for building JEdit documentation

diff -r 276befcd90d9 -r 011955e7846b Admin/mira.py
--- a/Admin/mira.py	Fri Jun 06 10:53:33 2014 +0200
+++ b/Admin/mira.py	Thu Jun 05 14:37:44 2014 +0200
@@ -98,10 +98,12 @@
 
     isabelle_home = paths[0]
 
+    home_user_dir = path.join(isabelle_home, 'home_user')
+    os.makedirs(home_user_dir)
+
     # copy over build results from dependencies
     heap_dir = path.join(isabelle_home, 'heaps')
     classes_dir = path.join(heap_dir, 'classes')
-    home_user_dir = path.join(isabelle_home, 'home_user')
     os.makedirs(classes_dir)
 
     for dep_path in dep_paths: