diff --git a/build.sh b/build.sh index 5e958ca..b9ebcfa 100644 --- a/build.sh +++ b/build.sh @@ -52,18 +52,18 @@ if [[ "$1" == "test" ]]; then ########## TEST ########## echo "Output generated as '$testOutput'" ### elif [[ "$1" == "install" ]]; then ########## INSTALL ########## + ### + echo "Installing header files..." + ### + + # Create why2 directory + if [[ ! -d $includeDirectory ]]; then + mkdir $includeDirectory + fi + + cp $includeFiles $includeDirectory + if [[ "$2" == "include" ]]; then - ### - echo "Installing header files..." - ### - - # Create why2 directory - if [[ ! -d $includeDirectory ]]; then - mkdir $includeDirectory - fi - - cp $includeFiles $includeDirectory - exit fi