diff --git a/documentation/src/development.dox b/documentation/src/development.dox index 071db9263..89d67f431 100644 --- a/documentation/src/development.dox +++ b/documentation/src/development.dox @@ -143,7 +143,7 @@ in the pdf output, whereas the html output uses different font sizes.