Skip to content

Flush archive file systems when removed#3510

Merged
aeisenberg merged 1 commit intomainfrom
aeisenberg/flush-archive-files
Mar 26, 2024
Merged

Flush archive file systems when removed#3510
aeisenberg merged 1 commit intomainfrom
aeisenberg/flush-archive-files

Conversation

@aeisenberg
Copy link
Copy Markdown
Contributor

This change will remove a file system archive from the cache when the associated folder is removed from the workspace.

This avoids the following bug:

  1. Import a database and add its source folder
  2. Remove the database (source folder is removed as well automatically).
  3. Change the source code and recreate the database
  4. Reimport the database and source folder
  5. BUG: You see the original source folder, not the new source folder

Replace this with a description of the changes your pull request makes.

Checklist

  • CHANGELOG.md has been updated to incorporate all user visible changes made by this pull request.
  • Issues have been created for any UI or other user-facing changes made by this pull request.
  • [Maintainers only] If this pull request makes user-facing changes that require documentation changes, open a corresponding docs pull request in the github/codeql repo and add the ready-for-doc-review label there.

@aeisenberg aeisenberg requested a review from a team as a code owner March 25, 2024 23:23
This change will remove a file system archive from the cache when the associated folder is removed from the workspace.

This avoids the following bug:

1. Import a database and add its source folder
2. Remove the database (source folder is removed as well automatically).
3. Change the source code and recreate the database
4. Reimport the database and source folder
5. BUG: You see the original source folder, not the new source folder
@aeisenberg aeisenberg force-pushed the aeisenberg/flush-archive-files branch from 2078b55 to e939750 Compare March 25, 2024 23:29
Copy link
Copy Markdown
Contributor

@norascheuch norascheuch left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍

@aeisenberg aeisenberg merged commit 5d45a11 into main Mar 26, 2024
@aeisenberg aeisenberg deleted the aeisenberg/flush-archive-files branch March 26, 2024 15:11
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.

3 participants