Unhide buffers that are marked dirty as a result of external modifications

Unhide buffers that are marked dirty as a result of external modifications

Several comments in the code point to the fact that hidden buffers are assumed
to be clean.

The other solution was to adapt the closing & saving code to take into account
hidden dirty buffers. Experience shows that it is more useful to unhide the
buffers at the moment of the external modification, in the context of a git
workflow where one has to reload the modified children buffers one-by-one.

Fixes crash at #10603