]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/graphs/tools/uri_set_queue.cgi
Initial revision
[helm.git] / helm / graphs / tools / uri_set_queue.cgi
index d84cdfde33f5b42b75148d325d53de9d354e7a3c..6a5d16ad51949042a9faaa82984004b0400549ef 100755 (executable)
@@ -5,7 +5,10 @@ use HTTP::Status;
 use HTTP::Response;
 use CGI;
 
-my $d = new HTTP::Daemon LocalPort => 8084;
+$urisetqueueport = $ENV{'URI_SET_QUEUE_PORT'} || $urisetqueueport;
+
+my $d = new HTTP::Daemon LocalPort => $urisetqueueport
+ or die "Error: port $urisetqueueport not available.";
 print "Please contact me at: <URL:", $d->url, ">\n";
 
 $SIG{CHLD} = "IGNORE"; # do not accumulate defunct processes