diff --git a/build.sh b/build.sh index 263b4c6..fc4e4d5 100644 --- a/build.sh +++ b/build.sh @@ -46,17 +46,19 @@ if [[ "$1" == "test" ]]; then ########## TEST ########## echo "Output generated as '$output'" ### elif [[ "$1" == "install" ]]; then ########## INSTALL ########## - ### - echo "Installing header files..." - ### + if [[ "$2" != "lib" ]]; then + ### + echo "Installing header files..." + ### - # Create why2 directory - if [[ ! -d $includeDirectory ]]; then - mkdir $includeDirectory + # Create why2 directory + if [[ ! -d $includeDirectory ]]; then + mkdir $includeDirectory + fi + + cp $includeFiles $includeDirectory fi - cp $includeFiles $includeDirectory - ### echo "Using '$compiler' as default compiler." ###