/src/Tools/VSCode/no_extension/ default tip
drwxr-xr-x [up]
drwxr-xr-x src
-rw-r--r-- 2022-07-01 20:47 +0200 655 README.md
-rw-r--r-- 2022-07-01 20:47 +0200 8465 isabelle.png
-rw-r--r-- 2022-07-01 20:47 +0200 60893 package-lock.json
-rw-r--r-- 2022-07-01 20:47 +0200 1112 package.json
-rw-r--r-- 2022-07-01 20:47 +0200 324 tsconfig.json