# 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,