aboutsummaryrefslogtreecommitdiff
path: root/plugins/derive/derive.mli
AgeCommit message (Expand)Author
2017-06-07Put all plugins behind an "API".Matej Kosik
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin