aboutsummaryrefslogtreecommitdiffstats
path: root/tools/ndfun.ml
Commit message (Expand)AuthorAgeFilesLines
* Use String.map instead of reimplementing it ourselves.Xavier Leroy2014-11-221-5/+18
* Merge of the nonstrict-ops branch:xleroy2012-01-141-0/+231