diff options
author | David Sherret <dsherret@users.noreply.github.com> | 2023-09-05 23:07:55 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2023-09-06 06:07:55 +0200 |
commit | a0af53fea134f712408fa2d2d20078dd8ca7d0e6 (patch) | |
tree | a7c3677f3937cc9194c0786da89969805e346be9 | |
parent | be1fc754a14683bf640b7bf0ecf6e286d02ee118 (diff) |
chore: pin third_party (#20386)
-rw-r--r-- | tools/util.js | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/util.js b/tools/util.js index 92ab18a7f..36f8dac14 100644 --- a/tools/util.js +++ b/tools/util.js @@ -138,7 +138,7 @@ export function getPrebuiltToolPath(toolName) { } const downloadUrl = - `https://raw.githubusercontent.com/denoland/deno_third_party/master/prebuilt/${platformDirName}`; + `https://raw.githubusercontent.com/denoland/deno_third_party/7f1a41fee1bfbffd56674269db8f1e19263cf751/prebuilt/${platformDirName}`; export async function downloadPrebuilt(toolName) { const spinner = wait("Downloading prebuilt tool: " + toolName).start(); |