Added Remove_Repository to supported command list

This feature was added in commit 70c03561bb90 but was
not added to the list of supported commands at the top
of file.  No functional change just a documentation
correction.

diff --git a/src/scripts/nightly/nightlybuild.sh b/src/scripts/nightly/nightlybuild.sh
index b73951b876547e98aeecfac119acd06e9e2f7433..bfbf9aa2c4e346fee2a0dd3d540f7dbdb9c3519e 100755 (executable)
--- a/src/scripts/nightly/nightlybuild.sh
+++ b/src/scripts/nightly/nightlybuild.sh
@@ -15,6 +15,7 @@
 # TESTSCRIPT   -       Run the testscript
 # SERVERSTOP   -       Stop the server if it was started by this script
 # CLEANUP      -       Remove the contents of the sandbox
 # TESTSCRIPT   -       Run the testscript
 # SERVERSTOP   -       Stop the server if it was started by this script
 # CLEANUP      -       Remove the contents of the sandbox

+# REMOVE_REPOSITORY    Removes the git repository when cleaning up

 #
 
 PROGNAME="$0"
 #
 
 PROGNAME="$0"