3 # This script copies BINARIES content into INSTALL, and substitute paths to enable extra compilation.
4 # If INSTALL already exists : does nothing!
5 if [ -d ¤{INSTALL_DIR} ]
7 echo Warning: ¤{INSTALL_DIR} already exists! Please rename or delete it before executing this script
10 if [ ! -d ¤{BINARIES_DIR} ]
12 echo Error: ¤{BINARIES_DIR} directory not found!
16 echo copies ¤{BINARIES_DIR} into ¤{INSTALL_DIR}
17 cp -RP ¤{BINARIES_DIR}/* ¤{INSTALL_DIR}
18 echo does the substitutions
19 # do the required substitutions