Rename misc ---> dev

Misc was a vague name.
pallene-lang · Jun 13, 2023 · 9ced050 · 9ced050
1 parent ecb0e0f
commit 9ced050
Show file tree

Hide file tree

Showing 4 changed files with 1 addition and 1 deletion.
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
@@ -83,7 +83,7 @@ If you change the ".pln" file of a benchmark please run the `./benchmarks/genera
 
 # Git workflow
 
-The `misc/` directory contains some scripts that I find useful in my day-to-day interactions with Git.
+The `dev/` directory contains some scripts that I find useful in my day-to-day interactions with Git.
 They are not required, but maybe you'll also find them useful.
 
 The `pre-commit` hook ensures that you never commit directly to the master branch,

diff --git a/misc/compute-authors.lua → dev/compute-authors.lua b/misc/compute-authors.lua → dev/compute-authors.lua
diff --git a/misc/git-sync → dev/git-sync b/misc/git-sync → dev/git-sync
diff --git a/misc/pre-commit → dev/pre-commit b/misc/pre-commit → dev/pre-commit