Merge branch 'master' into CGAL-Clean_CMakeLists.txt-GF

Author: MaelRL

.github/install.sh

@@ -1,5 +1,4 @@
 #!/bin/bash
-sudo add-apt-repository ppa:mikhailnov/pulseeffects -y
 sudo apt-get update
 sudo apt-get install -y  libmpfr-dev \
  libeigen3-dev qtbase5-dev libqt5sql5-sqlite libqt5opengl5-dev qtscript5-dev \

.github/workflows/Remove_labels.yml

@@ -0,0 +1,32 @@
+name: remove_labels
+on:
+  pull_request_target:
+    types: [synchronize]
+jobs:
+  remove_label:
+    runs-on: ubuntu-latest
+    if: contains(github.event.pull_request.labels.*.name, 'Tested')
+    name: remove label
+    steps:
+      - name: removelabel
+        uses: actions/github-script@v6
+        with:
+          github-token: ${{ secrets.GITHUB_TOKEN }}
+          script: |
+            github.rest.issues.removeLabel({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              issue_number: context.issue.number,
+              name: "Tested",
+            });
+      - name: Post address
+        uses: actions/github-script@v6
+        if: ${{ success() }}
+        with:
+          script: |
+            github.rest.issues.createComment({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              issue_number: context.issue.number,
+              body: "This pull-request was previously marked with the label `Tested`, but has been modified with new commits. That label has been removed."
+              })