diff options
Diffstat (limited to 'maude.install')
| -rw-r--r-- | maude.install | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/maude.install b/maude.install new file mode 100644 index 000000000000..750e4bd1acdd --- /dev/null +++ b/maude.install @@ -0,0 +1,8 @@ + ## arg 1: the new package version +post_install() { + echo + echo ">>> Copy maude.sh from /usr/share/maude/" + echo ">>> to /etc/profile.d/ to have" + echo ">>> MAUDE_LIB environment variable set at startup" + echo +} |