1 files changed, 11 insertions, 0 deletions
diff --git a/config_simple.sh b/config_simple.sh
new file mode 100755
index 00000000..52b7d1a6
--- /dev/null
+++ b/config_simple.sh
@@ -0,0 +1,11 @@
+arch=$1
+shift
+version=`git rev-parse --short HEAD`
+branch=`git rev-parse --abbrev-ref HEAD`
+date=`date +%Y-%m-%d`
+
+if test "x$CCOMP_INSTALL_PREFIX" = "x" ;
+then CCOMP_INSTALL_PREFIX=/opt/CompCert ;
+fi
+
+./configure --prefix ${CCOMP_INSTALL_PREFIX}/${branch}/${date}_${version}/$arch "$@" $arch