On Mi, 03 Feb 2016, LCD 47 wrote:
> On 3 February 2016, Bram Moolenaar <[email protected]> wrote:
> >
> > Lcd wrote:
> >
> > > On 3 February 2016, Danek Duvall <[email protected]> wrote:
> > > [...]
> > > > I think the most reliable thing to do here is to have a way to
> > > > know the pid and kill it directly, but since ! goes through
> > > > a shell, you don't have any way of knowing what the pid of
> > > > test_channel.py is.
> > >
> > > Or just make the server write its PID to a file with an unique
> > > name. This is still not ideal, but it's probably good enough for
> > > tests.
> >
> > Like we do for the port number. OK, that can work for now. But we
> > need job control functionality anyway. We should use that once it's
> > implemented.
> >
> > Vim can already start jobs, but currently always waits for them to
> > finish (with "!cmd" or system("cmd")). Should not be too difficult to
> > run a job in the background and get its PID. At least on Unix, not
> > sure about MS-Windows.
>
> Sure, job control is long overdue, but IMO it wouldn't be simple.
BTW: is it just me, or does it feel like rushing to integrate job
control now? I mean, its not like we don't have enough bugs waiting to
be fixed and it feels like integrating jobcontrol now into Vim is like
opening a whole new can of worms.
I apologize if I sounded overly pessimistic or un ungrateful. I really
enjoy the momentum that development currently gains, but perhaps those
patches should be integrated at the beginning of the 7.5 cycle, so they
have some time to flesh out correctly.
Best,
Christian
--
Vollkommene Künstler haben mehr dem Unterricht als der Natur zu
danken.
-- Goethe, Maximen und Reflektionen, Nr. 1352
--
--
You received this message from the "vim_dev" maillist.
Do not top-post! Type your reply below the text you are replying to.
For more information, visit http://www.vim.org/maillist.php
---
You received this message because you are subscribed to the Google Groups
"vim_dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
For more options, visit https://groups.google.com/d/optout.
