diff --git a/dev/clean.sh b/dev/clean.sh new file mode 100755 index 000000000..9da51bfb0 --- /dev/null +++ b/dev/clean.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +# Import reusable bits +pushd $( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd ) > /dev/null || exit 1 + . functions.sh +popd > /dev/null || exit 1 + +export ALIRE_OS=$(get_OS) + +gprclean -f -r -Palr_env.gpr diff --git a/dev/edit.sh b/dev/edit.sh index 66ca7ca90..a429fe80e 100755 --- a/dev/edit.sh +++ b/dev/edit.sh @@ -1 +1,8 @@ +# Import reusable bits +pushd $( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd ) > /dev/null || exit 1 + . functions.sh +popd > /dev/null || exit 1 + +export ALIRE_OS=$(get_OS) + gnatstudio -P alr_env & >/dev/null 2>&1