adapted to 7b318273a4aa;
authorwenzelm
Fri, 07 Aug 2020 22:28:04 +0200
changeset 72118 84f716e72fa3
parent 72117 4d8b3209dae3
child 72119 d115d50a19c0
adapted to 7b318273a4aa;
src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Fri Aug 07 22:23:40 2020 +0200
+++ b/src/Pure/ML/ml_process.scala	Fri Aug 07 22:28:04 2020 +0200
@@ -93,8 +93,7 @@
               ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
 
           List("Resources.init_session" +
-            "{pide = false" +
-            ", session_positions = " + print_sessions(sessions_structure.session_positions) +
+            "{session_positions = " + print_sessions(sessions_structure.session_positions) +
             ", session_directories = " + print_table(sessions_structure.dest_session_directories) +
             ", docs = " + print_list(base.doc_names) +
             ", global_theories = " + print_table(base.global_theories.toList) +