1#!/bin/bash 2 3set -e 4 5POLY_BASE="https://github.com/polyml/polyml" 6 7# Defaults: 8POLY_VERSION=${POLY_VERSION:-v5.7.1} 9POLY_GIT=${POLY_GIT:-F} 10POLY_ROOT=${POLY_ROOT:-F} 11 12PREFIX=$HOME 13if [ "$POLY_ROOT" == "T" ] 14then 15 PREFIX="/usr/" 16fi 17 18if [ "$POLY_GIT" == "T" ] 19then 20 git clone ${POLY_BASE}.git 21else 22 mkdir polyml 23 wget -qO- ${POLY_BASE}/archive/${POLY_VERSION}.tar.gz | \ 24 tar xvz -C polyml --strip-components 1 25fi 26 27cd polyml 28echo "*** Configuring PolyML for prefix: ${PREFIX}" 29./configure --prefix=$PREFIX 30make 31 32if [ "$POLY_GIT" == "T" ] 33then 34 make compiler 35fi 36 37if [ "$POLY_ROOT" == "T" -a "$UID" != "0" ] 38then 39 sudo make install 40else 41 make install 42fi 43 44if [ $(uname) = "Darwin" ] 45then 46 perl -pi -e 's/-R/-rpath /g' $HOME/bin/polyc 47fi 48