FIX #5819: add -XDataKinds to the language options section of the user's guide
authorJose Pedro Magalhaes <jpm@cs.uu.nl>
Fri, 27 Jan 2012 13:40:31 +0000 (14:40 +0100)
committerJose Pedro Magalhaes <jpm@cs.uu.nl>
Fri, 27 Jan 2012 13:40:31 +0000 (14:40 +0100)
commit3692c6f49530037744eee3c30fe0974e6de80135
tree5fbdeac3e6a6c989a914056788f531a02192246c
parentd16f5c74627eec1e2f30153bb56e0e9fbdcf64b8
FIX #5819: add -XDataKinds to the language options section of the user's guide
docs/users_guide/flags.xml