This MR introduces the following changes
- Automated replacement of file-placeholders in documentation using a simple python script. This allows to get rid of code blocks in cases where we copy over whole files.
Relates to the following issues
- First step towards #111 (closed)
The file placeholders of the form
§§§<filename>:<start>:<end>§§§ in the markdown file on the left will be replaced with the content of the actual files (from line
<start> to line
<end>), resulting in the docs page on the right. This all happens in the CI pipeline, such that the actual files of the repo are untouched.
make script more general such that we don't have to modify the ci config every time a new script needs replacements (probably the script should just go throught all documentation files)
add support for line numbers
change to syntax