aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc/about-hints
Commit message (Expand)AuthorAge
* Moving never-used comments from Zhints.v to dev/doc so as not toGravatar herbelin2011-10-01