Fix mistaken rename

I meant to rename the deploy script, not the deploy directory.
This commit is contained in:
Ben Sturmfels 2024-02-27 10:23:18 +11:00
parent a112ecd0ed
commit c9c1cd710b
13 changed files with 0 additions and 0 deletions