dist/U/lintlib.U

   1 ?RCS: $Id: lintlib.U 1 2006-08-24 12:32:52Z rmanfredi $
   2 ?RCS:
   3 ?RCS: Copyright (c) 1991-1997, 2004-2006, Raphael Manfredi
   4 ?RCS:
   5 ?RCS: You may redistribute only under the terms of the Artistic Licence,
   6 ?RCS: as specified in the README file that comes with the distribution.
   7 ?RCS: You may reuse parts of this distribution only within the terms of
   8 ?RCS: that same Artistic Licence; a copy of which may be found at the root
   9 ?RCS: of the source tree for dist 4.0.
  10 ?RCS:
  11 ?RCS: $Log: lintlib.U,v $
  12 ?RCS: Revision 3.0  1993/08/18  12:09:05  ram
  13 ?RCS: Baseline for dist 3.0 netwide release.
  14 ?RCS:
  15 ?MAKE:lintlib lintlibexp: Getfile Loc Oldconfig
  16 ?MAKE:  -pick add $@ %<
  17 ?S:lintlib:
  18 ?S:     This variable holds the name of the directory in which the user wants
  19 ?S:     to put public lint-library files for the package in question.  It is
  20 ?S:     most often a local directory such as /usr/local/lib/lint. Programs using
  21 ?S:     this variable must be prepared to deal with ~name expansion.
  22 ?S:.
  23 ?S:lintlibexp:
  24 ?S:     This variable is the same as the lintlib variable, but is filename
  25 ?S:     expanded at configuration time, for convenient use in your makefiles.
  26 ?S:.
  27 : determine where public lint libraries go
  28 case "$lintlib" in
  29 '') dflt=`./loc . "." /usr/local/lib/lint /usr/lib/lint /usr/lib`;;
  30 *) dflt="$lintlib" ;;
  31 esac
  32 echo " "
  33 fn=d~
  34 rp='Where do you want to put the public lint libraries?'
  35 . ./getfile
  36 lintlib="$ans"
  37 lintlibexp="$ansexp"
  38