Browse Source

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
master
Dave Parker 10 years ago
parent
commit
2026632c37
  1. 8
      prism/src/prism/ngprism.c

8
prism/src/prism/ngprism.c

@ -691,6 +691,14 @@ int main(int argc, char *argv[], char *env[]) {
nailgun_port = NAILGUN_PORT_DEFAULT; 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 /* 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 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 ng or ng.exe was used, since the appropriate nail should then handle

Loading…
Cancel
Save