# HG changeset patch
# User wenzelm
# Date 1645183121 -3600
# Node ID 2af8426e1f6500049ac1c1a3a35c2712e18c7e1f
# Parent  1e230ff31fb0044a4e5384728a0338c96c06d448
run Isabelle/VSCode using local VSCodium installation;

diff -r 1e230ff31fb0 -r 2af8426e1f65 lib/Tools/vscode
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/vscode	Fri Feb 18 12:18:41 2022 +0100
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: run Isabelle/VSCode using local VSCodium installation
+
+DIR="$(isabelle vscode_setup -C)" || exit "$?"
+exec "$DIR/bin/codium" \
+  --user-data-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS")" \
+  --extensions-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/extensions)" \
+  "$@"