Adding a page to the documentation

These pages are generated by Doxygen. If you want to add a new page, add a text file to the doc folder, ideally in the appropriate subfolder doc/dev for developer information, doc/user for user documentation.

At the beginning of the file, insert a line like this:

@page FileNameWithoutExtension The Title of the newly created page

The pages use Markdown for formatting.

In the end, you'll also need a link to get to your page. Go to the file where you want the link to appear, e.g. one of the index.md files. In there, add a snippet @ref FileNameWithoutExtension at the point where you want the link.