[jbosstools-issues] [JBoss JIRA] Commented: (JBIDE-1350) Cannot stop JBoss server instance when using non-standard JNDI port number