Conversation
|
I'm in the process of writing release notes. |
|
Most of these changes are my PRs, please let me know if you need any input. |
|
@kritzcreek would you be able to write release notes for the change #3799? I'm not sure I fully understand its implications. |
|
Sure, I'll try to explain it without talking about IDE internals: purs ide is better at reloading changesThe IDE would previously sometimes miss changes that were made outside of the editor, like building with new dependencies or recompiling larger parts of the project on the console. The IDE will now notice when this happened on the next command issued to it and refresh its state before processing that command. This might cause the first command after an external change to take a long time to execute, but should increase reliability in general. |
|
Thanks! |
|
Draft release notes: https://gist.github.com/hdgarrood/f0c167600036630bfe1c5fdb2729f3ca |
|
I say "draft" but as far as I'm concerned they're good to go, I'm just posting the link so that others can review. I think everything is now in place to go ahead with v0.13.7, so once this is approved I'll merge and do the release. |
2 participants
Resolves #3886. I've successfully backported all of the commits I listed in #3886 and pushed them to the 0.13.x branch in this repository already, which is why there's not much to see in this PR. This turned out to be relatively straightforward, thankfully!