manual: omit ocdoc/* during doc generation
authorDaniel Molkentin <daniel@molkentin.de>
Tue, 27 Jan 2015 22:29:49 +0000 (23:29 +0100)
committerDaniel Molkentin <daniel@molkentin.de>
Tue, 27 Jan 2015 22:35:45 +0000 (23:35 +0100)
commita9d12f3b1c2fc52a1025f9983d6f4793e61f853a
tree44dc7b8fc742a89cad2ee40455ea11bd635709a4
parent7d1839ee965b187f4ddcd8b6ab33ee6419b54d7e
manual: omit ocdoc/* during doc generation
user_manual/conf.py