Merge branch 'main' of https://gitlab.utwente.nl/dp-group-14/ide-plugin into main
No related branches found
No related tags found
Showing
- media/dark/preview.svg 1 addition, 0 deletionsmedia/dark/preview.svg
- media/dotview.js 24 additions, 7 deletionsmedia/dotview.js
- media/light/preview.svg 1 addition, 0 deletionsmedia/light/preview.svg
- package.json 18 additions, 0 deletionspackage.json
- src/commands.ts 34 additions, 9 deletionssrc/commands.ts
- src/extension.ts 8 additions, 3 deletionssrc/extension.ts
- src/sidebar.ts 29 additions, 22 deletionssrc/sidebar.ts
Loading
Please register or sign in to comment