aboutsummaryrefslogtreecommitdiffstats
path: root/debug/DebugTypes.mli
Commit message (Collapse)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