Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allow downloading multiple databases from GitHub #3073

Merged
merged 2 commits into from
Nov 21, 2023

Conversation

koesie10
Copy link
Member

@koesie10 koesie10 commented Nov 14, 2023

This adds the option to download multiple databases from GitHub in the initial GitHub database download prompt. The databases will be downloaded concurrently.

Unfortunately it doesn't seem possible to change the "OK" text in the quick pick to "Download", so I've left it as "OK" for now.

Screenshot 2023-11-14 at 16 14 43

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.

@koesie10 koesie10 force-pushed the koesie10/download-github-database branch from b190c35 to 636f8f1 Compare November 17, 2023 13:46
This adds the option to download multiple databases from GitHub in the
initial GitHub database download prompt. The databases will be
downloaded concurrently.

Unfortunately it doesn't seem possible to change the "OK" text in the
quick pick to "Download", so I've left it as "OK" for now.
@koesie10 koesie10 force-pushed the koesie10/download-multiple-github-databases branch from c20f0d9 to d0488dd Compare November 17, 2023 13:51
@koesie10 koesie10 marked this pull request as ready for review November 20, 2023 08:47
@koesie10 koesie10 requested a review from a team as a code owner November 20, 2023 08:47
@koesie10 koesie10 requested a review from starcke November 20, 2023 08:47
Base automatically changed from koesie10/download-github-database to main November 20, 2023 10:08
Copy link
Contributor

@starcke starcke left a comment

Choose a reason for hiding this comment

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

Looks good to me. Just a single question/comment.

selectedDatabases.map((database) =>
withProgress(
async (progress) => {
await downloadGitHubDatabaseFromUrl(
Copy link
Contributor

Choose a reason for hiding this comment

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

I found it slightly janky that it keeps selecting a new db when it has finished downloading. So when I download several
DBs I feel like I should be able to start immediately with the fastest one, but I dont think it is a big problem.

Copy link
Member Author

Choose a reason for hiding this comment

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

I think it's hard to do that since the selection is not controlled by this function itself. It sounds sound like a good idea, but maybe we can see if there's any feedback about this from users and implement something else based on that.

@koesie10 koesie10 merged commit 0523d2a into main Nov 21, 2023
14 checks passed
@koesie10 koesie10 deleted the koesie10/download-multiple-github-databases branch November 21, 2023 10:42
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