vdm-vscode icon indicating copy to clipboard operation
vdm-vscode copied to clipboard

Published 20 hours ago • verified publisher icon overturetool

didChange does not fire on git pull

Open FrederikPM opened this issue 2 years ago • 2 comments

If a VDM model is updated by pulling the source from GitHub, the Client doesn't seem to fire the usual "change watched file" events. So the server carries on with the "old" version, which can be confusing(!). If you restart the Client, then of course it's all fine.

This issue looks relevant, though different: https://github.com/microsoft/vscode/issues/72224

FrederikPM avatar May 05 '22 07:05 FrederikPM