proper orientation;
authorwenzelm
Mon, 02 Sep 2019 16:28:09 +0200
changeset 70829 ad7891a73230
parent 70828 f164cec7ac22
child 70830 5f4b8a505090
proper orientation;
src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Sep 02 11:46:27 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Sep 02 16:28:09 2019 +0200
@@ -233,7 +233,7 @@
             else true
           }
         } yield entry
-      Graph.make[Document.Node.Name, Options](used, permissive = true)(
+      Graph.make[Document.Node.Name, Options](used, symmetric = true, permissive = true)(
         Document.Node.Name.Theory_Ordering)
     }