# HG changeset patch
# User wenzelm
# Date 1568288344 -7200
# Node ID c1597167563ebe70002dff1b2533d5fb0ca97cc0
# Parent  60b1eda998f35f515b87dd80cf9a2c18fae89a91
avoid duplicate directories wrt. synthetic session;

diff -r 60b1eda998f3 -r c1597167563e 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,