From e1a017fb5c8d6acc39c2003a2646d61d0217e98a Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 7 Dec 2023 21:39:42 -0800 Subject: [PATCH] Remove doc build from regular regression This check is redundant in our CI since the bookrunner job already builds the documentation. It is also often breaking the regression job, maybe due to some disk requirement. --- scripts/kani-regression.sh | 8 -------- 1 file changed, 8 deletions(-) diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 161a96dbe1af..20782abe5cbc 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -100,14 +100,6 @@ FEATURES_MANIFEST_PATH="$KANI_DIR/tests/cargo-kani/cargo-features-flag/Cargo.tom cargo kani --manifest-path "$FEATURES_MANIFEST_PATH" --harness trivial_success cargo clean --manifest-path "$FEATURES_MANIFEST_PATH" -# Check that documentation compiles. -echo "Current disk usage:" -df -h -echo "Starting doc tests:" -cargo doc --workspace --no-deps --exclude std -echo "Disk usage after documentation build:" -df -h - echo echo "All Kani regression tests completed successfully." echo