avoid duplicate directories wrt. synthetic session;
authorwenzelm
Thu, 12 Sep 2019 13:39:04 +0200
changeset 70685 c1597167563e
parent 70684 60b1eda998f3
child 70686 9cde8c4ea5a5
avoid duplicate directories wrt. synthetic session;
src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Sep 12 13:35:53 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Sep 12 13:39:04 2019 +0200
@@ -493,7 +493,7 @@
             List(
               make_info(info.options,
                 dir_selected = false,
-                dir = info.dir,
+                dir = Path.explode("$ISABELLE_TMP_PREFIX"),
                 chapter = info.chapter,
                 Session_Entry(
                   pos = info.pos,