Jeremie Dimino
|
85ae1c75e4
|
Hack for latest odoc
|
2017-05-29 14:28:07 +01:00 |
|
Jeremie Dimino
|
500f224098
|
Delete old odoc artifacts before running odoc
|
2017-05-26 18:34:49 +01:00 |
Jeremie Dimino
|
37d7131a11
|
Simplify hack for not deleting odoc files
|
2017-05-26 18:34:49 +01:00 |
|
Jeremie Dimino
|
23f00abf18
|
Update odoc rules
|
2017-05-26 18:34:49 +01:00 |
|
Jeremie Dimino
|
d9165fc53e
|
Memoize a computation in odoc.ml
|
2017-05-26 18:34:49 +01:00 |
|
Jeremie Dimino
|
76d637fa74
|
Fix dependencies
|
2017-05-26 18:34:49 +01:00 |
|
Jeremie Dimino
|
43f413a59a
|
Support library indexes
|
2017-05-26 18:34:49 +01:00 |
|
Jeremie Dimino
|
7f8f4b23ee
|
Start of odoc rules
|
2017-05-26 18:34:49 +01:00 |