commandline option to exit restview if webbrowser doesn't poll anymore

[AvdN]

AFAICT the webpage that restview generates polls back for changes using JavaScript. It would be
useful to have a commandline-option/config-option/environmentvariable where you could specify
an amount X, so that if there was no polling for X seconds restview would exit. That way closing the
browser window is enough to stop the restview process.

I could take a shot at a PR if this is deemed useful.

[mgedmin]

Ooh, this is a nice idea. Exit when the browser tab gets closed. I like it.

Eagerly waiting for a PR.

User interface: I think command-line option is best here. Maybe --auto-exit, or --no-auto-exit since I probably want this on by default. Maybe also an --auto-exit-timeout=10, to specify the timeout in seconds, with the default being something reasonable (5? giving a chance to "undo close tab" quickly, if the user hits Ctrl-W on the wrong tab by accident).

[AvdN]

The default time doesn't have to be short, I just want to make sure I don't have to chase processes in some terminal tab. 60 seconds would be ok for me.

If you consider making this behaviour the default, then --auto-exit=0 could just switch the exit off.

[mgedmin]

Nah, I want --auto=exit=0 to mean exit immediately when the tab is closed.

(That would probably require a different mechanism -- e.g. an onbeforeunload event handler that tells the server-side that the tab is about to be closed -- to prevent false positives, but nevertheless I'd rather not overload 0 to mean something else.)