doc: fix a coding style error in the developer documentation.