chore(extras/depgraph): remove leandeps

There is no reason to implement this tool in Python anymore. If someone wants (I don't), they should do it in Lean, and store it as a Lean package in a separate git repository. Closes leanprover#1744
leodemoura · Jul 15, 2017 · b093b3c · b093b3c
1 parent 1d6716d
commit b093b3c
Show file tree

Hide file tree

Showing 3 changed files with 0 additions and 256 deletions.
diff --git a/extras/depgraph/README.md b/extras/depgraph/README.md
diff --git a/extras/depgraph/leandeps.py b/extras/depgraph/leandeps.py
diff --git a/extras/depgraph/leandeps.sh b/extras/depgraph/leandeps.sh