Commit | Line | Data |
---|---|---|
d8875586 MBT |
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 |