From 5f6f1e2e8d6543745ff73daa4b5b1df71eef87fb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?S=C3=A9bastien=20Loriot?= <sebastien.loriot@cgal.org>
Date: Mon, 14 Nov 2022 20:14:55 +0100
Subject: [PATCH] remove line that seems useless

---
 .github/install.sh | 1 -
 1 file changed, 1 deletion(-)

diff --git a/.github/install.sh b/.github/install.sh
index e06328da401..32b8552aa8f 100755
--- a/.github/install.sh
+++ b/.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 \