Skip to content
Find file
Fetching contributors…
Cannot retrieve contributors at this time
29 lines (22 sloc) 798 Bytes
#!!!!You need to source me with "source" from the _RIGHT_ directory!!!!
if [ ! -r ]
then echo "There is no here.
Are you sure you run this script from the source directory ?
# 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
# 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.