diff options
Diffstat (limited to 'development/splint/doinst.sh')
| -rw-r--r-- | development/splint/doinst.sh | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/development/splint/doinst.sh b/development/splint/doinst.sh deleted file mode 100644 index 15d8003421..0000000000 --- a/development/splint/doinst.sh +++ /dev/null @@ -1,7 +0,0 @@ -# If we do not have a lint already: -if ! command -v lint 1> /dev/null 2> /dev/null ; then - # Make this the default - ( cd /usr/bin ; ln -sf splint lint ) - ( cd /usr/man/man1 ; ln -sf splint.1.gz lint.1.gz ) -fi - |