diff options
| author | Maxime Dénès | 2015-12-14 13:33:47 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2015-12-14 13:37:01 +0100 |
| commit | 469cb750c6c1aa46f77b2a89a36f79f29aa97073 (patch) | |
| tree | 03ea46d4888936d910b2c56e82b64859b10e5832 /kernel/type_errors.ml | |
| parent | c377938a8f87d9c0517aa0c7d4564323951a2133 (diff) | |
Revert PMP's fix of #2498, which introduces an incompatibility with lablgtk
2.14. Debian ships with lablgtk 2.16 only since a few months, so we apply the
fix to trunk instead.
This reverts commits:
490160d25d3caac1d2ea5beebbbebc959b1b3832.
ef8718a7fd3bcd960d954093d8c636525e6cc492.
6f9cc3aca5bb0e5684268a7283796a9272ed5f9d.
901a9b29adf507370732aeafbfea6718c1842f1b.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions