diff options
Diffstat (limited to 'src/ci')
| -rwxr-xr-x | src/ci/run.sh | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/ci/run.sh b/src/ci/run.sh index e3f38e4834a..afa6d1fa0ae 100755 --- a/src/ci/run.sh +++ b/src/ci/run.sh @@ -105,7 +105,15 @@ fi travis_fold end log-system-info if [ ! -z "$SCRIPT" ]; then - sh -x -c "$SCRIPT" + # FIXME(#49246): Re-enable these tools after #49246 has been merged and thus fixing the cache. + if [ "$DEPLOY_ALT" = 1 ]; then + sh -x -c "$SCRIPT \ + --exclude src/tools/rls \ + --exclude src/tools/rustfmt \ + --exclude src/tools/clippy" + else + sh -x -c "$SCRIPT" + fi else do_make() { travis_fold start "make-$1" |