pkill directly rather than fool around with a CGI

kill.cgi has been broken for a while, and the Makefile has the wrong URI
for dev anyway.

svn path=/trunk/packages/invirt-web/; revision=2183

diff --git a/code/Makefile b/code/Makefile
index 270a871..ee8bbd9 100644 (file)
--- a/code/Makefile
+++ b/code/Makefile
@@ -7,7 +7,7 @@ chmod:
        chmod -R g+w . 2>/dev/null || true
 
 kill:
-       wget http://xvm.mit.edu/kill.cgi -O /dev/null -nv || true
+       pkill main.fcgi
 
 compile:
        for dir in $(DIRS); do \

diff --git a/code/kill.cgi b/code/kill.cgi
deleted file mode 100755 (executable)
index f297d32..0000000
--- a/code/kill.cgi
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/bin/sh
-pkill main.fcgi
-echo "Content-Type: text/plain"
-echo
-echo "Killed."