3 commits

Author	SHA1	Message	Date
Juerd Waalboer	45f12a9354	Fix saving files in text editor ... It stored the old content, so effectively not changing the file. I don't really understand why *this* was the version I committed, because I was sure I tested it and it worked :)	2022-09-06 23:48:55 +02:00
Juerd Waalboer	042db97ea8	editor: only ask to save if anything's changed; print status	2022-08-30 20:57:41 +02:00
Juerd Waalboer	43a1990974	bump to v3.5; add built-in editor	2022-08-30 20:45:01 +02:00