Merge remote branch 'origin/master' into edge

AdaCore · May 7, 2024 · a4f1818 · a4f1818
2 parents 735cd7b + 9281244
commit a4f1818
Showing 1 changed file with 0 additions and 37 deletions.
diff --git a/.vscode/tasks.json b/.vscode/tasks.json
@@ -1,50 +1,13 @@
 {
    "version": "2.0.0",
    "tasks": [
-      {
-         "label": "build",
-         "type": "shell",
-         "command": "gprbuild",
-         "args": ["-p", "-P", "${config:ada.projectFile}", "-cargs", "-gnatef"],
-         "problemMatcher": ["$ada"],
-         "group": {
-            "kind": "build",
-            "isDefault": true
-         }
-      },
       {
          "label": "Run tests",
          "type": "shell",
          "command": "make check",
          "problemMatcher": ["$ada"],
          "group": "test"
       },
-      {
-         "type": "shell",
-         "label": "ada: Compile current file",
-         "command": "gprbuild",
-         "args": [
-            "-q",
-            "-f",
-            "-c",
-            "-u",
-            "${file}",
-            "-P",
-            "${config:ada.projectFile}",
-            "-cargs",
-            "-gnatef"
-         ],
-         "problemMatcher": "$ada",
-         "presentation": {
-            "echo": true,
-            "reveal": "silent",
-            "revealProblems": "onProblem",
-            "focus": false,
-            "panel": "shared",
-            "showReuseMessage": true,
-            "clear": true
-         }
-      },
       {
          "type": "ada",
          "configuration": {