On Fri, Oct 25, 2019 at 7:49 AM Julian Foad <[email protected]> wrote:
> > How can we best insert this into 'downloads.html', at the right place? Various code generation tools (e.g. GUI designers) that are designed not to clobber user edits insert their generated code between special comments. So in download.html there might be comments like: <!-- BEGIN AUTOMATICALLY GENERATED CODE --> ... <!-- END AUTOMATICALLY GENERATED CODE --> and the script would search for those and replace what's between them.
