tuned -- Date.Format.default used by toString;
authorwenzelm
Tue, 11 Oct 2016 21:25:10 +0200
changeset 64151 be9b3cffe058
parent 64150 b10f2ddd7679
child 64152 8f5b23536c56
tuned -- Date.Format.default used by toString;
src/Pure/System/options.scala
src/Pure/Tools/build_history.scala
--- a/src/Pure/System/options.scala	Tue Oct 11 20:54:42 2016 +0200
+++ b/src/Pure/System/options.scala	Tue Oct 11 21:25:10 2016 +0200
@@ -407,8 +407,7 @@
         .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
 
     Isabelle_System.mkdirs(Options.PREFS_DIR)
-    File.write_backup(Options.PREFS,
-      "(* generated by Isabelle " + Date.Format.default(Date.now()) + " *)\n\n" + prefs)
+    File.write_backup(Options.PREFS, "(* generated by Isabelle " + Date.now() + " *)\n\n" + prefs)
   }
 }
 
--- a/src/Pure/Tools/build_history.scala	Tue Oct 11 20:54:42 2016 +0200
+++ b/src/Pure/Tools/build_history.scala	Tue Oct 11 21:25:10 2016 +0200
@@ -62,7 +62,7 @@
 
       Isabelle_System.mkdirs(etc_settings.dir)
       File.write(etc_settings,
-        "# generated by Isabelle " + Date.Format.default(Date.now()) + "\n" +
+        "# generated by Isabelle " + Date.now() + "\n" +
         "#-*- shell-script -*- :mode=shellscript:\n")
 
       val component_settings =