Patch | Description | Author | Forwarded | Bugs | Origin | Last update |
---|---|---|---|---|---|---|
0001-Ignore-in-font-maps.patch | Ignore "'''" in font maps This token may appear and makes mlpost choke, but seems irrelevant. |
Stephane Glondu <steph@glondu.net> | no | 2021-12-03 | ||
0002-Upgrade-to-ppxlib.patch | Upgrade to ppxlib | =?utf-8?q?Cl=C3=A9ment_Pascutto?= <clement@pascutto.fr> | no | debian | upstream, https://github.com/backtracking/mlpost/commit/66fd02f89de9cb72dbc0241ad0b748761c35c7be | 2021-04-07 |
0003-Input-mp-tool.mpiv-instead-of-metafun.mp-in-generate.patch | Input mp-tool.mpiv instead of metafun.mp in generated files This seems needed since update of context to version 2023.05.05.20230730+dfsg-2. |
Stephane Glondu <steph@glondu.net> | no | debian | https://bugs.debian.org/1052298 | 2023-09-22 |