Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
tree: c6a61f5876
Fetching contributors…

Cannot retrieve contributors at this time

28 lines (22 sloc) 0.797 kb
#!!!!You need to source me with "source env.sh" from the _RIGHT_ directory!!!!
if [ ! -r main.ml ]
then echo "There is no main.ml here.
Are you sure you run this script from the source directory ?
";
fi
# To compile the source, using pad installation.
echo setting PATH
export PATH=/home/pad/packages/Linux/bin:/home/pad/packages/bin:$PATH
echo setting LD_LIBRARY_PATH
export LD_LIBRARY_PATH=/home/pad/packages/Linux/lib:$LD_LIBRARY_PATH
export PATH=/usr/lib64/openmpi/1.2.5-gcc/bin:$PATH
export LD_LIBRARY_PATH=/usr/lib64/openmpi/1.2.5-gcc/lib:$LD_LIBRARY_PATH
# for faster compiler
echo setting OPTBIN
export OPTBIN=.opt
# for exception stack traces
echo setting OCAMLRUNPARAM
export OCAMLRUNPARAM="b"
# To run. To find the config/ files.
echo setting PFFF_HOME
export PFFF_HOME=`pwd`
Jump to Line
Something went wrong with that request. Please try again.