[Øyvind Harboe]
> Some questions before then:
>
> Do you believe that I've found a real problem in the /etc/init.d/jetty
> script?

No idea.  Didn't spend enough time on the issue. :)

>> What about adding pidfile support to jetty?  It sound like the correct
>> place to fix it.
>
> I don't know what it means to add "pidfile support to jetty". Jetty is a
> platform independent Java program...

It mean adding some code looking like this when the program starts:

  pidfile = "/var/run/jetty.pid";
  mypid = system.getpid();
  writepidfile(pidfile, mypid);

And code like this when the program stops:

  system.removefile(pidfile);

Keep in mind that I do no longer remember the library API in java. :)

No need to CC me.  I'm on the list. :)

Reply via email to