Closed gasche closed 11 years ago
I haven't tried to build the doc. Please tell me if some other changes are needed, I can rebase this commit.
No need to build the doc for such a trivial change. What could possibly go wrong? (famous last words, I know).
Merged.
I haven't tried to build the doc. Please tell me if some other changes are needed, I can rebase this commit.