path: root/mcon/U/lintlib.U
diff options
Diffstat (limited to 'mcon/U/lintlib.U')
1 files changed, 38 insertions, 0 deletions
diff --git a/mcon/U/lintlib.U b/mcon/U/lintlib.U
new file mode 100644
index 0000000..09107a1
--- /dev/null
+++ b/mcon/U/lintlib.U
@@ -0,0 +1,38 @@
+?RCS: $Id$
+?RCS: Copyright (c) 1991-1997, 2004-2006, Raphael Manfredi
+?RCS: You may redistribute only under the terms of the Artistic Licence,
+?RCS: as specified in the README file that comes with the distribution.
+?RCS: You may reuse parts of this distribution only within the terms of
+?RCS: that same Artistic Licence; a copy of which may be found at the root
+?RCS: of the source tree for dist 4.0.
+?RCS: $Log: lintlib.U,v $
+?RCS: Revision 3.0 1993/08/18 12:09:05 ram
+?RCS: Baseline for dist 3.0 netwide release.
+?MAKE:lintlib lintlibexp: Getfile Loc Oldconfig
+?MAKE: -pick add $@ %<
+?S: This variable holds the name of the directory in which the user wants
+?S: to put public lint-library files for the package in question. It is
+?S: most often a local directory such as /usr/local/lib/lint. Programs using
+?S: this variable must be prepared to deal with ~name expansion.
+?S: This variable is the same as the lintlib variable, but is filename
+?S: expanded at configuration time, for convenient use in your makefiles.
+: determine where public lint libraries go
+case "$lintlib" in
+'') dflt=`./loc . "." /usr/local/lib/lint /usr/lib/lint /usr/lib`;;
+*) dflt="$lintlib" ;;
+echo " "
+rp='Where do you want to put the public lint libraries?'
+. ./getfile