diff options
Diffstat (limited to 'wrapper.sh')
-rwxr-xr-x | wrapper.sh | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/wrapper.sh b/wrapper.sh new file mode 100755 index 000000000000..aa31a9d36e84 --- /dev/null +++ b/wrapper.sh @@ -0,0 +1,5 @@ +#!/bin/sh + +LIBPATH=/usr/share/inform7 +INFORM7="$LIBPATH/inform7" +$INFORM7 --no-census-update -internal $LIBPATH "$@" |