aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2015-01-17 20:35:43 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2015-01-17 20:35:43 +0100
commit4a96baf41965249c77b390dd252e8fa36b806c5f (patch)
treee003fc27bdd641d3aa7414b92fd3c6c492e1cbf0 /library/library.ml
parent5e5d51762df0e34769225e8c59c77b97b1212c29 (diff)
Fix #3379, now that Require inside modules is allowed again.
Diffstat (limited to 'library/library.ml')
0 files changed, 0 insertions, 0 deletions