/src/Tools/VSCode/patches/ default tip
drwxr-xr-x [up]
-rw-r--r-- 2022-07-01 20:47 +0200 1034 cli.patch
-rw-r--r-- 2022-07-01 20:47 +0200 2598 isabelle_encoding.patch
-rw-r--r-- 2022-07-01 20:47 +0200 4637 isabelle_encoding.ts
-rw-r--r-- 2022-07-01 20:47 +0200 2331 no_ocaml_icons.patch