aboutsummaryrefslogtreecommitdiff
path: root/test-suite/coqdoc/bug5648.v
AgeCommit message (Collapse)Author
2017-07-19Removing testing unsupported Next.Hugo Herbelin
2017-07-17Adding a coqdoc target to test-suite.Hugo Herbelin
One file was already ready for testing. We add another one. Note that we have to remove the machine-dependent lines in the output tex files.