Skip to content
Permalink
Browse files

Used a DUNE_DIR_EXCLUDE variable to exclude unecessary directories (e…

….g. sosa variant not selected for build)
  • Loading branch information...
sagotch committed Jul 24, 2019
1 parent 670a708 commit dd73aebeeca58b49c3cd1ed77673e76a3ce4d386
Showing with 8 additions and 0 deletions.
  1. +1 −0 Makefile
  2. +5 −0 configure
  3. +2 −0 lib/dune.in
@@ -72,6 +72,7 @@ CPPO_D=$(API_D) $(GWDB_D)
-e "s/%%%API_PKG%%%/$(API_PKG)/g" \ -e "s/%%%API_PKG%%%/$(API_PKG)/g" \
-e "s/%%%SOSA_PKG%%%/$(SOSA_PKG)/g" \ -e "s/%%%SOSA_PKG%%%/$(SOSA_PKG)/g" \
-e "s/%%%GWDB_PKG%%%/$(GWDB_PKG)/g" \ -e "s/%%%GWDB_PKG%%%/$(GWDB_PKG)/g" \
-e "s/%%%DUNE_DIRS_EXCLUDE%%%/$(DUNE_DIRS_EXCLUDE)/g" \
> $@ > $@


hd/etc/version.txt: hd/etc/version.txt:
@@ -17,6 +17,7 @@ API_PKG=
GWDB_D= GWDB_D=
GWDB_PKG= GWDB_PKG=
SOSA_PKG= SOSA_PKG=
DUNE_DIRS_EXCLUDE=


while [[ $# -ne 0 ]]; do while [[ $# -ne 0 ]]; do
case $1 in case $1 in
@@ -27,8 +28,10 @@ while [[ $# -ne 0 ]]; do
GWDB_D="-D GWDB1" ; GWDB_D="-D GWDB1" ;
GWDB_PKG="geneweb.gwdb1_internal geneweb.gwdb1" ;; GWDB_PKG="geneweb.gwdb1_internal geneweb.gwdb1" ;;
--sosa-num) --sosa-num)
DUNE_DIRS_EXCLUDE="$DUNE_DIRS_EXCLUDE sosa.array sosa.zarith"
SOSA_PKG="geneweb.sosa-num" ;; SOSA_PKG="geneweb.sosa-num" ;;
--sosa-zarith) --sosa-zarith)
DUNE_DIRS_EXCLUDE="$DUNE_DIRS_EXCLUDE sosa.array sosa.num"
SOSA_PKG="geneweb.sosa-zarith" ;; SOSA_PKG="geneweb.sosa-zarith" ;;
*) *)
echo -e "\\x1b[33m[WARNING]\\x1b[0m Option $1 unknown and ignored.";; echo -e "\\x1b[33m[WARNING]\\x1b[0m Option $1 unknown and ignored.";;
@@ -44,6 +47,7 @@ fi ;


if [[ $SOSA_PKG == "" ]] ; then if [[ $SOSA_PKG == "" ]] ; then
echo -e "\\x1b[33m[WARNING]\\x1b[0m SOSA is not set, using geneweb.sosa" ; echo -e "\\x1b[33m[WARNING]\\x1b[0m SOSA is not set, using geneweb.sosa" ;
DUNE_DIRS_EXCLUDE="$DUNE_DIRS_EXCLUDE sosa.num sosa.zarith" ;
SOSA_PKG="geneweb.sosa" ; SOSA_PKG="geneweb.sosa" ;
fi ; fi ;


@@ -111,6 +115,7 @@ print_vars() {
echo "GWDB_D=${GWDB_D}" echo "GWDB_D=${GWDB_D}"
echo "GWDB_PKG=${GWDB_PKG}" echo "GWDB_PKG=${GWDB_PKG}"
echo "SOSA_PKG=${SOSA_PKG}" echo "SOSA_PKG=${SOSA_PKG}"
echo "DUNE_DIRS_EXCLUDE=${DUNE_DIRS_EXCLUDE}"
} }


print_makefile() { print_makefile() {
@@ -1,3 +1,5 @@
(dirs :standard \ %%%DUNE_DIRS_EXCLUDE%%%)

(library (library
(name geneweb) (name geneweb)
(public_name geneweb) (public_name geneweb)

0 comments on commit dd73aeb

Please sign in to comment.
You can’t perform that action at this time.