diff --git a/bin/install_module b/bin/install_module index bdb3129d54aee95b53e700b83f625f1d249a8975..07c4292da1b91eb850d9a03d1e0a4643a253f7fb 100755 --- a/bin/install_module +++ b/bin/install_module @@ -2,6 +2,18 @@ # install_module <from> <to> +if [ "$1" = "--help" ] ; then +cat <<EOF + Installs a module (.pmod file or directory, or a .so file) + in a destination directory. Called by "make install". + + Usage: + + install_module source destination_directory +EOF +exit 0 +fi + FROM="$1" TO="$2"