diff options
author | 2017-03-24 16:15:32 +0100 | |
---|---|---|
committer | 2017-03-24 16:15:32 +0100 | |
commit | af291869bb7d1184d8e655906572d75937ca829b (patch) | |
tree | 62a5ccf9ee7b115b7d1118cbc3db92c553261713 /printing/printing.mllib | |
parent | 3234a893a1b3cfd6b51f1c26cc10e9690d8a703e (diff) | |
parent | 7535e268f7706d1dee263fdbafadf920349103db (diff) |
Merge branch 'trunk' into pr379
Diffstat (limited to 'printing/printing.mllib')
-rw-r--r-- | printing/printing.mllib | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/printing/printing.mllib b/printing/printing.mllib index b0141b6d3..86b68d8fb 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -1,6 +1,5 @@ Genprint Pputils -Ppannotation Ppconstr Printer Printmod |