Skip to content

Commit

Permalink
Remove doc build from regular regression (#2925)
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.


Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com>
  • Loading branch information
celinval and jaisnan committed Dec 8, 2023
1 parent 63af43d commit d26485a
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 d26485a

Please sign in to comment.