diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-17 00:11:42 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-17 00:11:42 +0100 |
| commit | 1b111e3658b3f79a9814fd9799e2dbe0a921c768 (patch) | |
| tree | 2f68e86ec69d2a68e31b23a345a41ee794e24aad /config_simple.sh | |
| parent | d0326db1105704e02e2b40facc2a85a267a2b9b5 (diff) | |
| download | compcert-kvx-1b111e3658b3f79a9814fd9799e2dbe0a921c768.tar.gz compcert-kvx-1b111e3658b3f79a9814fd9799e2dbe0a921c768.zip | |
specify prefix with CCOMP_INSTALL_PREFIX
Diffstat (limited to 'config_simple.sh')
| -rwxr-xr-x | config_simple.sh | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/config_simple.sh b/config_simple.sh index f02680c4..e2d3844c 100755 --- a/config_simple.sh +++ b/config_simple.sh @@ -3,4 +3,9 @@ shift version=`git rev-parse --short HEAD` branch=`git rev-parse --abbrev-ref HEAD` date=`date -I` -./configure --prefix /opt/CompCert/${branch}/${date}_${version}/$arch "$@" $arch + +if test "x$CCOMP_INSTALL_PREFIX" = "x" ; +then CCOMP_INSTALL_PREFIX=/opt/CompCert ; +fi + +./configure --prefix ${CCOMP_INSTALL_PREFIX}/${branch}/${date}_${version}/$arch "$@" $arch |