Closed DenisCarriere closed 8 years ago
Tip for future: this is the exception when you can and should force push an amended commit. Or commit new ones and squash all of the together. GitHub will pick up the change in the same PR. Of course you can't do that from the web.
Thanks for the tip.
Once the PR is merged to DefinitelyTyped
https://github.com/DefinitelyTyped/DefinitelyTyped/pull/10921