diff options
author | 2017-09-04 17:29:14 +0200 | |
---|---|---|
committer | 2017-09-04 17:29:14 +0200 | |
commit | d752838ae24dd431f9f2f8de09b5635139ecf3b5 (patch) | |
tree | 0eb0e324051c936d400a3f4cfe016bdd2e921145 /pretyping/recordops.ml | |
parent | 3072bd9d080984833f5eb007bf15c6e9305619e3 (diff) | |
parent | a4d63bfe7d8b5025321a3c0ad5f4d13758bfbd56 (diff) |
Merge PR #1018: Avoid reinstalling some Cygwin dependencies on AppVeyor.
Diffstat (limited to 'pretyping/recordops.ml')
0 files changed, 0 insertions, 0 deletions