clarified options;
authorwenzelm
Mon, 14 Oct 2019 21:44:07 +0200
changeset 71058 bbb7d69f7a4d
parent 71057 4c8e28dabbc4
child 71059 1d063b7f7928
clarified options;
src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Mon Oct 14 21:00:04 2019 +0200
+++ b/src/Pure/Tools/update.scala	Mon Oct 14 21:44:07 2019 +0200
@@ -22,7 +22,7 @@
 
     context.build_logic(logic)
 
-    val path_cartouches = context.session_options.bool("update_path_cartouches")
+    val path_cartouches = context.options.bool("update_path_cartouches")
 
     def update_xml(xml: XML.Body): XML.Body =
       xml flatMap {