20 Oct
2023
20 Oct
'23
5:53 p.m.
On Fri Oct 20 17:24:45 2023 +0000, Gabriel Ivăncescu wrote:
That would require changing update_window_doc and create_document_node to handle it, is that fine?
That seems fine to me.