#!/bin/bash
# 
# This script copies BINARIES content into INSTALL, and substitute paths to enable extra compilation. 
# If INSTALL already exists : does nothing!
if [ -d INSTALL ]
then
    echo Warning: INSTALL already exists! Please rename or delete it before executing this script
    exit
fi
if [ ! -d ¤{BINARIES_DIR} ]
then
    echo Error: ¤{BINARIES_DIR} directory not found!
    exit
fi
mkdir INSTALL
echo copies ¤{BINARIES_DIR} into INSTALL
cp -RP ¤{BINARIES_DIR}/*  INSTALL
echo does the substitutions
# do the required substitutions
¤{SUBSTITUTION_LOOP}