author | wenzelm |
Mon, 14 Oct 2019 21:44:07 +0200 | |
changeset 70868 | bbb7d69f7a4d |
parent 70867 | 4c8e28dabbc4 |
child 70869 | 1d063b7f7928 |
--- 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 {