diff options
Diffstat (limited to 'lang/polyml/files/poly.in')
| -rw-r--r-- | lang/polyml/files/poly.in | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/lang/polyml/files/poly.in b/lang/polyml/files/poly.in deleted file mode 100644 index 3fa3f863eaa..00000000000 --- a/lang/polyml/files/poly.in +++ /dev/null @@ -1,9 +0,0 @@ -#!/bin/sh - -USERDB="$HOME/.polyml/ML_dbase" -if [ ! -f "$USERDB" ]; then - USERDB="" -fi - -exec %%PREFIX%%/lib/polyml/poly $USERDB $* - |