From 2026632c37af03bbe9bb3b6f5d2e5db830679914 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 27 Aug 2015 10:19:51 +0000 Subject: [PATCH] ngprism: Allow the use of "ngprism stop" to kill the server. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10591 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/ngprism.c | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/prism/src/prism/ngprism.c b/prism/src/prism/ngprism.c index 88ddd90a..430b8f54 100644 --- a/prism/src/prism/ngprism.c +++ b/prism/src/prism/ngprism.c @@ -691,6 +691,14 @@ int main(int argc, char *argv[], char *env[]) { nailgun_port = NAILGUN_PORT_DEFAULT; } + /* if executing just the ng client with no arguments or -h|--help, then + display usage and exit. Don't handle -h|--help if a command other than + ng or ng.exe was used, since the appropriate nail should then handle + --help. */ + if (argc > 1 && strcmp("stop", argv[1]) == 0) { + cmd = "ng-stop"; + } + /* if executing just the ng client with no arguments or -h|--help, then display usage and exit. Don't handle -h|--help if a command other than ng or ng.exe was used, since the appropriate nail should then handle