diff options
| author | Théo Zimmermann | 2018-03-28 18:23:48 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-04-08 20:46:10 +0200 |
| commit | e332bf0d9685679f4c5415bec7681fd948921fb5 (patch) | |
| tree | 4e07e6ead8d8a5643d727adee25b2ee22fc29e00 /kernel/nativelambda.ml | |
| parent | 7d3e3f0aa5aea66a5e3c884eb0642a317d762051 (diff) | |
Merge script does not warn when the remote is set to HTTPS.
This should solve Emilio's problem.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions