Conversation
|
Hey, thanks for sending this. The diff is in a file that is generated as part of our export process and the person who works on that is out for a couple of weeks. I'll get back to you when I can figure something out. |
|
Why do you want to remove this dependency? Here's what I got by asking around internally:
Since our best guess is that it fixes something in a scenario that we don't routinely test, I don't want to remove it unless it's actively causing problems somewhere else. |
|
In macOS it prevents installation because gcc is missing. |
|
Why not use |
|
@xclerc wdyt? |
|
Looking at the opam repository, it may I think it is fine to change to However, @ncihnegn, could you give |
|
|
Thanks; I have never seen that on I would suggest to change to |
|
Thanks, Xavier, I will change to |
|
This change has been released internally. I've asked how long it'll take to make its way to github. I know the export is all automated now so I wouldn't expect that to take long. |
|
Ah, sorry, there is a manual step I didn't know about. It'll be about a month before you see the change on github. |
No description provided.