Skip to content

Commit

Permalink
ci-run.sh: install gcc requirements for debian if not in docker
Browse files Browse the repository at this point in the history
  • Loading branch information
tgingold committed Jun 2, 2024
1 parent a16bc62 commit ce5b53f
Showing 1 changed file with 5 additions and 3 deletions.
8 changes: 5 additions & 3 deletions scripts/ci-run.sh
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,6 @@ set -e
ISGPL=false
ISSYNTH=true
USEDOCKER=false
SUDO=sudo

# Transform long options to short ones
for arg in "$@"; do
Expand All @@ -68,7 +67,7 @@ while getopts ":b:p:cdgs" opt; do
case $opt in
b) BACK=$OPTARG ;;
c) enable_color;;
d) USEDOCKER=true; unset SUDO;;
d) USEDOCKER=true;;
g) ISGPL=true;;
p) PKG_NAME=$OPTARG;;
s) ISSYNTH=false;;
Expand Down Expand Up @@ -219,7 +218,10 @@ build () {
echo "$gccURL"
mkdir gcc-srcs
curl -L "$gccURL" | tar -xz -C gcc-srcs --strip-components=1
$SUDO apt-get -y install --no-install-recommends libgmp-dev libmpfr-dev libmpc-dev
if [ "$USEDOCKER" != "true" ]; then
# Add requirements for debian
sudo apt-get -y install --no-install-recommends libgmp-dev libmpfr-dev libmpc-dev
fi

gend

Expand Down

0 comments on commit ce5b53f

Please sign in to comment.