Skip to content

Commit

Permalink
Add a script.sh file to run scripts (#6047)
Browse files Browse the repository at this point in the history
### What was changed?
Add a script.sh file to run scripts

### How has this been tested?
Manually ran the shell file with a few different commands

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
keyboardDrummer authored Jan 13, 2025
1 parent 416575a commit b79708e
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions script.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
dotnet run --project Source/Scripts/Scripts.csproj -- "$@"

0 comments on commit b79708e

Please sign in to comment.