-
Sylvain Dailler authored
Remove now selects the parent of the removed node when a selected node is contained in the removed subtree. Adding a function that check a request is not referring to obsolete node_id in itp_server.ml. If such a request is found, the error that owuld have been generated is not sent to the ide.
373a7bc9