aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/globnames.mli
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-10-30 23:48:30 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-13 18:11:22 +0100
commit6bd240fce21c172680a0cec5346b66e08c76418a (patch)
tree640407a38cc96645a66ccb7754ace80092fdfe22 /library/globnames.mli
parent8d176db01baf9fb4a5e07decb9500ef4a8717e93 (diff)
[ci] [coq] Complete 4.06.0 support.
Due to an API change in laglgtk, we need to update CoqIDE. We use a makefile hack so it can compile with lablgtk < 2.8.16, another option would be to require 2.8.16 as a minimal dependency. We also refactor travis to test more lablgtk versions. We also need to account for improved attribute handling in 4.06.0, in particular module aliases will propagate the deprecation status. Fixes #6140.
Diffstat (limited to 'library/globnames.mli')
0 files changed, 0 insertions, 0 deletions