changeset 81024 | d1535ba3b1ca |
parent 65977 | c51b74be23b6 |
child 81049 | 45ef41e823f7 |
--- a/src/Tools/VSCode/etc/options Wed May 01 11:12:59 2024 +0200 +++ b/src/Tools/VSCode/etc/options Wed May 01 12:30:53 2024 +0200 @@ -29,3 +29,6 @@ option vscode_caret_preview : bool = false -- "dynamic preview of caret document node" + +option vscode_html_output : bool = false + -- "output State and Output in HTML"