--- a/src/Tools/VSCode/extension/README.md Tue Mar 07 10:52:04 2017 +0100
+++ b/src/Tools/VSCode/extension/README.md Tue Mar 07 13:55:49 2017 +0100
@@ -28,5 +28,5 @@
Symbols Mode. It needs to be configured manually as follows:
$ISABELLE_HOME/src/Tools/VSCode/extension/isabelle-symbols.json contains a
-configuration (generated via `isabelle vscode_symbols`). Its content needs to
+configuration (generated via `isabelle build_vscode`). Its content needs to
be copied carefully into the regular VSCode User Preferences.