Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829unset -f cargo 2>/dev/null || true
# Determine the directory that this script is inif [ "$BASH_VERSION" ]; then SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"elif [ "$ZSH_VERSION" ]; then SCRIPT_DIR="$( cd "$( dirname "${(%):-%N}" )" >/dev/null 2>&1 && pwd )"else echo "Unknown shell; exiting." return 1fi
echo "building vargo"( cd "$SCRIPT_DIR/vargo" || exit 1 cargo build --release || exit 1) || return 1
export PATH="$SCRIPT_DIR/vargo/target/release:$PATH"
echo "WARNING: Vargo is being deprecated. Use Cargo instead. Refer to BUILD.md."echo " See also: https://github.com/verus-lang/verus/pull/2686"
function cargo { echo "when working on Verus do not use cargo directly, use vargo instead" 1>&2 echo "if you need to, you can still access cargo directly by starting a new shell without running the activate command" 1>&2 return 1}