Closed louib closed 4 years ago
nevermind, just saw it's actually hosted in the main repo.
@louib Thanks for the pull request. Meanwhile the manual is no longer maintained in the source repository, hence I picked your commit and applied it manually in 98bc73b0546fda10917ca141afdd9ac8550d96b8.
Linking to the website's repository for issues and pull request made on the manual, instead of the main repository.
@hvhaugwitz thanks for reviewing :eyes: