Skip to content

Do not write heading in readme with capitals.

Robbert Krebbers requested to merge robbert/smaller_iris into master

Currently it says "IRIS", having the potential to let some people think it's an acronym.

Also, in general, headings of level 1 are already displayed with bigger font size in the Gitlab rendering of the markdown, so there's no need to put more emphasis.

Merge request reports