@kugel- BTW your runtime suggestion is fine too.
But one question that applies to both it and any script is how to know where the digits in the `version.txt` split, past contents have been `3211`. So without human intervention how will a script/program know if it is 3.21.1 (correct) or 3.2.11 (incorrect) or something else?
If it needs human intervention it can't be runtime or makefile or configure, it could only be at `update-scintilla.sh` time.