Skip to content

Commit

Permalink
update readme and docs
Browse files Browse the repository at this point in the history
  • Loading branch information
adomani committed Oct 31, 2024
1 parent 001369c commit 974532a
Showing 1 changed file with 4 additions and 0 deletions.
4 changes: 4 additions & 0 deletions scripts/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,10 @@ to learn about it as well!
**Tool for manual maintenance**
- `fix_unused.py`
Bulk processing of unused variable warnings, replacing them with `_`.
- `add_deprecations.sh` is a text-based script that automatically adds deprecation stateements.
It assumes that the only difference between master and the current status of the PR consists
of renames. More precisely, any change on a line that contains a declaration name
and is not a rename, will likely confuse the script.

**Analyzing Mathlib's import structure**
- `unused_in_pole.sh` (followed by an optional `<target>`, defaulting to `Mathlib`)
Expand Down

0 comments on commit 974532a

Please sign in to comment.