diff options
-rwxr-xr-x | git-tools/setup_github_network.php | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/git-tools/setup_github_network.php b/git-tools/setup_github_network.php index ae3d34f5fe..9ada9e437a 100755 --- a/git-tools/setup_github_network.php +++ b/git-tools/setup_github_network.php @@ -31,14 +31,15 @@ function show_usage() echo " -r repository_name Overwrites the repository name (optional)\n"; echo " -m your_github_username Sets up ssh:// instead of git:// for pushable repositories (optional)\n"; echo " -d Outputs the commands instead of running them (optional)\n"; + echo " -h This help text\n"; exit(1); } // Handle arguments -$opts = getopt('s:u:r:m:d'); +$opts = getopt('s:u:r:m:dh'); -if (empty($opts)) +if (empty($opts) || isset($opts['h'])) { show_usage(); } |