!4#3115

Stream: mathlib4

[Newell Jensen]

@Eric Wieser So I opened !4#3115 but then back tracked on it as I think it will take me too long and probably better that I start on something easier. I deleted the PR on github but seems like the port status is still showing the file as in progress. Does the port status dashboard have a certain amount of time it needs before it gets updated? If it is easier for me to restore the PR, that is also possible. Just wanted to give a heads up so that this file doesn't seem to be in progress on the dashboard when it isn't (at least not from me).

[Eric Wieser]

#port-dashboard is updated every 30 minutes

[Eric Wieser]

In future, there's not much point pushing the PR until you've looked at how many errors there are and decided if you're likely going to be able to fix (some of) them

[Newell Jensen]

Eric Wieser said:

In future, there's not much point pushing the PR until you've looked at how many errors there are and decided if you're likely going to be able to fix (some of) them

Couldn't agree more