Use different scratch folders for different repos

[rwestberg]

Hi all,

Please review this small change that ensures that different repositories get different scratch folders when inspected by the pullrequest bot, which should increase performance.

Best regards,
Robin

Progress

• Change must not contain extraneous whitespace
• Change must be properly reviewed

Approvers

• Erik Helin (ehelin - Reviewer)

[bridgekeeper]

👋 Welcome back rwestberg! A progress list of the required criteria for merging this PR into master will be added to the body of your pull request.

[edvbld]

Looks good!

[openjdk]

@rwestberg This change now passes all automated pre-integration checks. When the change also fulfills all project specific requirements, type /integrate in a new comment to proceed. After integration, the commit message will be:

Use different scratch folders for different repos

Reviewed-by: ehelin

• If you would like to add a summary, use the /summary command.
• To credit additional contributors, use the /contributor command.
• To add additional solved issues, use the /solves command.

➡️ To integrate this PR with the above commit message, type /integrate in a new comment.

[rwestberg]

/integrate

[openjdk]

@rwestberg
Pushed as commit 9e9559a.

[mlbridge]

Webrevs

• 00: Full (9e02092)