Hi all,
I have an feature request for the GUI editor (veeery handy for testing, thanks!): make it possible to revert files from disk. I have a file open in it that I want to update, because it got modified externally. But I can't -- not even if I open the open-file dialog and try to open it again, as if. No go, the old version sits in the editor still, and I was lucky not to overlook this fact or else I wouldn't know why it doesn't work.
Thanks for considering this, and thanks for your work on BaseX,
Piotr