Skip to content

Conversation

odow
Copy link
Member

@odow odow commented Jul 10, 2020

Following the lead of jump-dev/JuMP.jl#2269

@odow odow merged commit a95e7d6 into master Jul 10, 2020
@odow odow deleted the odow-patch-1 branch July 10, 2020 23:43
@blegat blegat added this to the v0.9.15 milestone Jul 12, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

2 participants