unset -f cargo 2>/dev/null || true

# Determine the directory that this script is in
if [ "$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 1
fi

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
}