Martin von Zweigbergk 38180555de working_copy: keep track of operation ID (#13) ... When there are concurrent operations that want to update the working copy, it's useful to know which operation was the last to successfully update the working copy. That can help use decide how to resolve a mismatch between the repo view's record and the working copy's record. If we detect such a difference, we can look at the working copy's operation ID to see if it was updated by an operation before or after we loaded the repo. If the working copy's record says that it was updated at operation A and we have loaded the repo at operation B (after A), we know that the working copy is stale, so we can automatically update it (or tell the user to run some command to update it if we think that's more user-friendly). Conversely, if we have loaded the repo at operation A and the working copy's record says that it was updated at operation B, we know that there was some concurrent operation that updated it. We can then decide to print a warning telling the user that we skipped updating because of the conflict. We already have logic for not updating the working copy if the repo is loaded at an earlier operation, but maybe we can drop that if we record the operation in the working copy (as this patch does).		2022-01-19 19:15:29 -08:00
..
op_store.proto	git: start tracking HEAD of underlying Git repo	2021-12-01 11:08:53 -08:00
store.proto	backend: remove unused Commit::is_pruned (#32)	2021-10-06 23:53:15 -07:00
working_copy.proto	working_copy: keep track of operation ID (#13)	2022-01-19 19:15:29 -08:00