chore: delete obsolete porting scripts (#14346)

This is a more conservative version of #14314, deleting just the scripts that we should have deleted a year ago when the port finished.
leanprover-community · Jul 2, 2024 · d490030 · d490030
1 parent d180e67
commit d490030
Show file tree

Hide file tree

Showing 5 changed files with 0 additions and 527 deletions.
diff --git a/scripts/align-import.py b/scripts/align-import.py
diff --git a/scripts/align.py b/scripts/align.py
diff --git a/scripts/benchmark.sh b/scripts/benchmark.sh
diff --git a/scripts/make_port_status.py b/scripts/make_port_status.py