Workaround issue with devtoolset sudo (pytorch#1022)

jpvillam-amd · Aug 4, 2022 · af7c2e5 · af7c2e5
1 parent 57f8a60
commit af7c2e5
Showing 1 changed file with 8 additions and 1 deletion.
diff --git a/.circleci/docker/common/install_user.sh b/.circleci/docker/common/install_user.sh
@@ -22,5 +22,12 @@ chown jenkins:jenkins /usr/local
 # TODO: Maybe we shouldn't
 echo 'jenkins ALL=(ALL) NOPASSWD:ALL' > /etc/sudoers.d/jenkins
 
+# Work around bug where devtoolset replaces sudo and breaks it.
+if [ -n "$DEVTOOLSET_VERSION" ]; then
+  SUDO=/bin/sudo
+else
+  SUDO=sudo
+fi
+
 # Test that sudo works
-sudo -u jenkins sudo -v
+$SUDO -u jenkins $SUDO -v