Closed infotroph closed 4 months ago
cc @DongchenZ since I believe you're the main user of this script -- any reason this can't live alongside other installation tools in scripts/?
scripts/
Sorry I have no idea about this.
@infotroph since this script isn't used by anyone, or called by anything else, I think we can just delete it rather than move it
cc @DongchenZ since I believe you're the main user of this script -- any reason this can't live alongside other installation tools in
scripts/
?