mira: USER_HOME must exist for building JEdit documentation
authornoschinl
Thu, 05 Jun 2014 14:37:44 +0200
changeset 57179 011955e7846b
parent 57178 276befcd90d9
child 57180 74c81a5b5a34
mira: USER_HOME must exist for building JEdit documentation
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: