#!/bin/sh
: '$Id$'

: Create a lint library file. The name of the library file is constructed
: from the first argument. The second argument indicates the directory where
: the result is to be placed. This version is for Unix lint.

n=$1
shift
d=$1
shift
/usr/bin/lint -C$n $*
mv llib-l$n.ln $d
