author | wenzelm |
Wed, 23 Mar 2022 17:24:09 +0100 | |
changeset 75316 | d7f41034a239 |
parent 75315 | 5c0ea94757f2 |
child 75317 | 8fcf57708636 |
--- a/src/Tools/VSCode/src/vscode_main.scala Wed Mar 23 16:53:00 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_main.scala Wed Mar 23 17:24:09 2022 +0100 @@ -204,7 +204,7 @@ def add_option(opt: String): Unit = options = options ::: List(opt) val getopts = Getopts(""" -Usage: isabelle vscode [OPTIONS] [-- VSCODE_OPTIONS ...] +Usage: isabelle vscode [OPTIONS] [ARGUMENTS] [-- VSCODE_OPTIONS] -A NAME ancestor session for option -R (default: parent) -C run as foreground process, with console output