From 4be38d930d7e1836435f0d28b8f7dec6eb0f9e16 Mon Sep 17 00:00:00 2001 From: ENGO150 <v.smejkal06@gmail.com> Date: Mon, 2 May 2022 19:19:43 +0200 Subject: [PATCH] added lib sub-flag --- build.sh | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) 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." ###