Remove obsolete add_stars.sh

RichardLitt · Jul 9, 2018 · 42b2b7c · 42b2b7c
1 parent 1e8bd08
commit 42b2b7c
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 9 deletions.
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
@@ -12,7 +12,6 @@ Please feel free to contribute in any way you can: by submitting links, by engag
 - Alphabetize your entry.
 - If a language entry for your specific tool does not exist, please create one.
 - Update the Table of Contents if you can. This can be done automatically with [`doctoc`](https://github.com/thlorenz/doctoc).
-- To add the GitHub Star badge, run `cd tooling; sh add_stars.sh`.
 - Check that your links work. We will automatically catch any broken links using TravisCI.
 
 If any of this is arduous, please open a PR with what you have and we can work together to make it fit.

diff --git a/tooling/add_stars.sh b/tooling/add_stars.sh