Jérémie Dimino e56fba9a57 Do not use opam-installer to copy files (#941) ... Instead of calling opam-installer, manually parse .install files and copy the files. Signed-off-by: Jeremie Dimino <jeremie@dimino.org>		2018-07-03 10:10:09 +01:00
..
boot	Do not use opam-installer to copy files (#941)	2018-07-03 10:10:09 +01:00
cmdliner	Remove most useless parentheses from the syntax (#915)	2018-06-27 16:38:05 +01:00
opam-file-format/src	Remove most useless parentheses from the syntax (#915)	2018-06-27 16:38:05 +01:00
re	Remove most useless parentheses from the syntax (#915)	2018-06-27 16:38:05 +01:00
update-cmdliner.sh	Don't stop on the first error (#477)	2018-02-06 14:39:03 +00:00
update-opam-file-format.sh	Imported opam-file-format	2017-05-08 16:56:21 +01:00
update-re.sh	Add a script to upgrade vendor/re	2017-05-02 14:08:47 +01:00
update-usexp.sh	Vendored usexp and switch to it	2017-12-21 13:13:47 +00:00