This repository has been archived by the owner on Dec 14, 2021. It is now read-only.

Refresh just one file #1187

Open

egraether opened this issue Jun 16, 2021 · 0 comments

Labels

feature

Contributor

egraether commented Jun 16, 2021

E.g. a file affected by a fatal error.

egraether added the feature label

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