From d26485a3436ce96793a6e63aace0de6bd0d81810 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 8 Dec 2023 08:41:40 -0800 Subject: [PATCH] Remove doc build from regular regression (#2925) This check is redundant in our CI since the bookrunner job already builds the documentation. It is also often breaking the regression job. Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> --- 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