← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to configure

  • Committer: Package Import Robot
  • Author(s): Stéphane Glondu
  • Date: 2012-01-03 23:42:48 UTC
  • mfrom: (1.2.4)
  • Revision ID: package-import@ubuntu.com-20120103234248-p9r8h1579n67v55a
Tags: 8.3pl3-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
configure
6
6
# 
7
7
##################################
8
8
 
9
 
VERSION=8.3pl2
 
9
VERSION=8.3pl3
10
10
VOMAGIC=08300
11
11
STATEMAGIC=58300
12
12
DATE=`LANG=C date +"%B %Y"`
321
321
 
322
322
MAKE=`which make`
323
323
if [ "$MAKE" != "" ]; then
324
 
  MAKEVERSION=`$MAKE -v | head -1`
325
 
  case $MAKEVERSION in
326
 
    "GNU Make 3.8"[12])
327
 
      echo "You have GNU Make >= 3.81. Good!";;
328
 
    *)
 
324
  MAKEVERSION=`$MAKE -v | head -1 | cut -d" " -f3`
 
325
  MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1`
 
326
  MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2`
 
327
  if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then
 
328
      echo "You have GNU Make $MAKEVERSION. Good!"
 
329
  else
329
330
      OK="no"
330
331
      if [ -x ./make ]; then
331
332
          MAKEVERSION=`./make -v | head -1`
346
347
      else
347
348
          echo "You have locally installed GNU Make 3.81. Good!"
348
349
      fi
349
 
  esac
 
350
  fi
350
351
else
351
 
  echo "Cannot find GNU Make 3.81."
 
352
  echo "Cannot find GNU Make >= 3.81."
352
353
fi
353
354
 
354
355
# Browser command
659
660
 
660
661
if test "$with_doc" = "all" 
661
662
then
662
 
    for cmd in "latex" "hevea" "pngtopnm" "pnmtops" ; do
 
663
    for cmd in "latex" "hevea" ; do
663
664
        if test ! -x "`which $cmd`"
664
665
        then 
665
666
            echo "$cmd was not found; documentation will not be available"
1084
1085
echo "*Warning* To compile the system for a new architecture"
1085
1086
echo "          don't forget to do a 'make archclean' before './configure'."
1086
1087
 
1087
 
# $Id: configure 14025 2011-04-19 07:19:00Z notin $
 
1088
# $Id: configure 14833 2011-12-19 21:57:30Z notin $