- FETCH_COMMIT=$(git ls-remote https://github.com/rust-lang/rust/ HEAD | cut -f 1)
- # We can't pull from a commit with josh
- # (https://github.com/josh-project/josh/issues/1034), so we just hope that
- # nothing gets merged into rustc *during* this pull.
- git fetch http://localhost:8000/rust-lang/rust.git$JOSH_FILTER.git master
- # Just verify that `master` didn't move.
- if [[ $FETCH_COMMIT != $(git ls-remote https://github.com/rust-lang/rust/ HEAD | cut -f 1) ]]; then
- echo "Looks like something got merged into Rust *while we were pulling*. Aborting. Please try again."
+ FETCH_COMMIT="$1"
+ if [ -z "$FETCH_COMMIT" ]; then
+ FETCH_COMMIT=$(git ls-remote https://github.com/rust-lang/rust/ HEAD | cut -f 1)