From a52f87021f78520370845a62063caa6d9b2cf3b2 Mon Sep 17 00:00:00 2001
From: Alejandro R Mosteo <amosteo@unizar.es>
Date: Fri, 24 May 2024 14:42:54 +0200
Subject: [PATCH] new dev/clean.sh (#1686)

---
 dev/clean.sh | 10 ++++++++++
 dev/edit.sh  |  7 +++++++
 2 files changed, 17 insertions(+)
 create mode 100755 dev/clean.sh

diff --git a/dev/clean.sh b/dev/clean.sh
new file mode 100755
index 00000000..9da51bfb
--- /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 66ca7ca9..a429fe80 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
-- 
2.39.5