4 Commits

Author	SHA1	Message	Date
Jérémie Dimino	239ff0054e	Remove jbuilder_ prefix for vendored libraries (#720) ... It's not useful since we are not installing them. Also unwrap libraries that are unwrapped upstream.	2018-04-24 14:38:30 +01:00
Jérémie Dimino	27a299437d	4.02.3 compatiblity	2017-02-26 21:28:30 +00:00
Jeremie Dimino	193f8d5238	moved cmdliner and re to vendor/	2017-02-21 15:09:58 +00:00
Jeremie Dimino	2357fa0799	114.20+69	2016-12-15 11:20:46 +00:00