etc/options
changeset 76578 06b001094ddb
parent 76474 287c3adcdcd6
child 76972 6c542f2aab85
--- a/etc/options	Tue Dec 06 14:41:13 2022 +0100
+++ b/etc/options	Tue Dec 06 16:23:49 2022 +0100
@@ -220,6 +220,9 @@
 public option editor_output_state : bool = false
   -- "implicit output of proof state"
 
+public option editor_document_session : string = ""
+  -- "session for interactive document preparation"
+
 option editor_execution_delay : real = 0.02
   -- "delay for start of execution process after document update (seconds)"