# HG changeset patch
# User wenzelm
# Date 1571082247 -7200
# Node ID bbb7d69f7a4dc4536d15fbeeaa410dbfeee2144e
# Parent  4c8e28dabbc45b90670a0eebb1f6b9ae6c6d0a2d
clarified options;

diff -r 4c8e28dabbc4 -r bbb7d69f7a4d 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 {