configure-gmp

#!/bin/sh
#*=====================================================================*/
#*    serrano/prgm/project/bigloo/bigloo/gmp/configure-gmp             */
#*    -------------------------------------------------------------    */
#*    Author      :  Manuel Serrano                                    */
#*    Creation    :  Mon Sep  7 09:49:25 2009                          */
#*    Last change :  Wed Dec 11 08:47:56 2019 (serrano)                */
#*    Copyright   :  2009-19 Manuel Serrano                            */
#*    -------------------------------------------------------------    */
#*    Ad-hoc configuration for GMP.                                 */
#*=====================================================================*/

echo "configure gmp with \"CC=$cc ./configure --libdir=$libdir/$fildir --includedir=$libdir/fildir --bindir=$bootdir/BGLINSTALLTMP --docdir=$docdir --mandir=$mandir --infodir=$infodir $gmpconfigureopt\"" >> ../configure.log

src=$gmpversion
(cd $src && \
 export CC=$cc && \
 ./configure  --libdir=$libdir/$fildir --includedir=$libdir/$fildir --bindir=$bootdir/BGLINSTALLTMP --docdir=$docdir --mandir=$mandir --infodir=$infodir $gmpconfigureopt 2>&1 >> ../../configure.log && \
 cp gmp.h $bootdir/lib/bigloo/$release || \
 (echo "configure gmp fail, see configure.log file." && exit 1)) || exit 1