# HG changeset patch
# User wenzelm
# Date 1648052649 -3600
# Node ID d7f41034a239c23ef83273b98bc01b89b627cecf
# Parent  5c0ea94757f265897d7c3fbec7539377a4c13229
tuned message;

diff -r 5c0ea94757f2 -r d7f41034a239 src/Tools/VSCode/src/vscode_main.scala
--- 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