# HG changeset patch
# User wenzelm
# Date 1357762901 -3600
# Node ID b93484db43edc440713884e64527b891be3db124
# Parent  b7e38c13d87b23c4904f590b5355422472aa168b
create required PREFS_DIR;

diff -r b7e38c13d87b -r b93484db43ed src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Wed Jan 09 18:35:51 2013 +0100
+++ b/src/Pure/System/options.scala	Wed Jan 09 21:21:41 2013 +0100
@@ -63,8 +63,9 @@
   private val SECTION = "section"
   private val OPTION = "option"
   private val OPTIONS = Path.explode("etc/options")
-  private val PREFS = Path.explode("$ISABELLE_HOME_USER/etc/preferences")
-  private val PREFS_BACKUP = Path.explode("$ISABELLE_HOME_USER/etc/preferences~")
+  private val PREFS_DIR = Path.explode("$ISABELLE_HOME_USER/etc")
+  private val PREFS = PREFS_DIR + Path.basic("preferences")
+  private val PREFS_BACKUP = PREFS_DIR + Path.basic("preferences~")
 
   lazy val options_syntax =
     Outer_Syntax.init() + ":" + "=" + "--" +
@@ -347,6 +348,7 @@
       changed.sortBy(_._1)
         .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
 
+    Options.PREFS_DIR.file.mkdirs()
     Options.PREFS.file renameTo Options.PREFS_BACKUP.file
     File.write(Options.PREFS,
       "(* generated by Isabelle " + Calendar.getInstance.getTime + " *)\n\n" + prefs)