Skip to content

Commit

Permalink
Update with suggestions
Browse files Browse the repository at this point in the history
  • Loading branch information
keertk committed Oct 2, 2023
1 parent 5ceed83 commit 8edd0a7
Showing 1 changed file with 15 additions and 10 deletions.
25 changes: 15 additions & 10 deletions scripts/release.py
Original file line number Diff line number Diff line change
Expand Up @@ -18,16 +18,21 @@
import wget
import json

def generate_release_info(platform, artifacts):
return ("\n" +
"http_archive(\n"
" name = \"remote_" + platform + "\",\n" +
" sha = \"" + artifacts["sha"] + "\",\n" +
" urls = [\n" +
" \"" + artifacts["mirror_url"] + "\",\n" +
" \"" + artifacts["github_url"] + "\",\n" +
" ],\n" +
")")
def generate_release_info(platform, artifacts):
return '''
http_archive(
name = "remote_{platform}",
sha256 = "{sha}",
urls = [
"{mirror_url}",
"{github_url}"
]
)'''.format(
platform = platform,
sha = artifacts["sha"],
mirror_url = artifacts["mirror_url"],
github_url = artifacts["github_url"]
)

def download_file(mirror_url):
wget.download(mirror_url , '.')
Expand Down

0 comments on commit 8edd0a7

Please sign in to comment.