update readme and docs

scripts/README.md

@@ -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`)

scripts/add_deprecations.sh

@@ -1,5 +1,23 @@
 #! /bin/bash
 
+: <<'BASH_MODULE_DOCS'
+
+The script contained in this file tries to automatically generate deprecations for declarations that were renamed in a PR.
+
+The script is entirely text-based, so it makes several simplifying assumptions and may be easily confused.
+
+# Assumptions
+
+The script works under the assumption that the only modifications between master and the current branch are renames of lemmas that should be deprecated.
+
+The script inspects the relevant git diff, extracts the old name and the new one and uses this information to insert deprecated aliases as needed.
+
+Most other differences may confuse the script, although there is some slack.
+
+Please, do not try to push the boundaries of the script, since it is quite simple-minded!
+
+BASH_MODULE_DOCS
+
 if [ -z "${1}" ]
 then
   commit="$( git merge-base master "$( git rev-parse --abbrev-ref HEAD )" )"