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)"