aboutsummaryrefslogtreecommitdiffstats
path: root/debug/DebugTypes.mli
Commit message (Expand)AuthorAgeFilesLines
* bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-141-3/+3
* Moved the types defined by the Debug Interface into a separate file.Bernhard Schommer2015-10-011-0/+160