Skip to content

Commit

Permalink
new dev/clean.sh (#1686)
Browse files Browse the repository at this point in the history
  • Loading branch information
mosteo committed May 24, 2024
1 parent b4044b9 commit a52f870
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 0 deletions.
10 changes: 10 additions & 0 deletions dev/clean.sh
Original file line number Diff line number Diff line change
@@ -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
7 changes: 7 additions & 0 deletions dev/edit.sh
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit a52f870

Please sign in to comment.