Skip to content

Commit

Permalink
Remove doc build from regular regression
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
celinval committed Dec 8, 2023
1 parent 01bf411 commit e1a017f
Showing 1 changed file with 0 additions and 8 deletions.
8 changes: 0 additions & 8 deletions scripts/kani-regression.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit e1a017f

Please sign in to comment.