function ensure_decent_gcc_on_deb {
# point gcc to the one offered by distro if the used one is different
- local old=$(readlink -e /usr/bin/x86_64-linux-gnu-gcc | cut -d'-' -f2)
+ local old=$(readlink -e /usr/bin/gcc | cut -d'-' -f2)
local new=$1
- if dpkg --compare-versions $old eq $new; then
+ if [ ! -f /usr/bin/gcc-${old} ]; then
+ $SUDO rm -f /usr/bin/gcc-${old}
+ $SUDO ln -sf /usr/bin/gcc-${new} /usr/bin/gcc
+ return
+ elif dpkg --compare-versions $old eq $new; then
return
fi
*i*)
# interactive shell
cat <<EOF
-/usr/bin/x86_64-linux-gnu-gcc now points to gcc-$old, which is not the version
-shipped with the distro: gcc-$new. Reverting...
+/usr/bin/gcc now points to gcc-$old, which is not the version shipped with the
+distro: gcc-$new. Reverting...
EOF
esac