Skip to content

Fix refresh#84

Merged
japaric merged 1 commit into
rust-lang:editorfrom
vojtechkral:fix-refresh
Jun 6, 2014
Merged

Fix refresh#84
japaric merged 1 commit into
rust-lang:editorfrom
vojtechkral:fix-refresh

Conversation

@vojtechkral

Copy link
Copy Markdown
Contributor

Reinitialize the editor when navigating.

japaric pushed a commit that referenced this pull request Jun 6, 2014
@japaric japaric merged commit 80fa864 into rust-lang:editor Jun 6, 2014
@japaric

japaric commented Jun 6, 2014

Copy link
Copy Markdown

Awesome! Thanks.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants