Merge branch 'main' of https://gitlab.utwente.nl/dp-group-14/ide-plugin into main (dc31dc77) · Commits · DP-Group 14 / IDE-Plugin · GitLab

Skip to content

GitLab

Explore

Sign in

Primary navigation

Project

I

IDE-Plugin
- Activity
- Members
- Labels
- Issues
- Issue boards
- Milestones
- Iterations
- Wiki
- Requirements
- Environments
- Terraform modules
- Incidents
- Service Desk

Snippets Groups Projects

Admin message

This server will be unavailable due to maintenance on March 19, 2025 between 20:00 and 22:00 (Central European Time). We are sorry for the inconvenience. During this period, neither Git nor the GitLab web interface will be available, so please make sure you plan accordingly.

dc31dc77

Commit dc31dc77 authored 4 years ago by Sytze de Witte

Downloads
- Plain Diff

Merge branch 'main' of https://gitlab.utwente.nl/dp-group-14/ide-plugin into main

parents 72c7aefc 9953b6fd

No related branches found

No related tags found

Loading

Changes 3

Hide whitespace changes

Inline Side-by-side

Showing

media/modest-icon.png 0 additions, 0 deletions

media/modest-icon.png
package.json 6 additions, 4 deletions

package.json
src/extension.ts 3 additions, 2 deletions

src/extension.ts

with 9 additions and 6 deletions

Loading

0% Loading or .

You are about to add 0 people to the discussion. Proceed with caution.

Finish editing this message first!

Please register or sign in to comment