* ui: move get_datetime tool to frontend
* clarify docs
* server: drop the now unused ctime include
strftime() and gmtime_r() were the only users, both went away with the
get_datetime tool. Also make the renderer's catch inert: the browser
executor always emits JSON, so a non-JSON result is no longer a date to
display.
---------
Co-authored-by: Pascal <[email protected]>