1 files changed, 5 insertions, 0 deletions
diff --git a/tools/rename-bins b/tools/rename-bins
new file mode 100755
index 0000000..a613278
--- /dev/null
+++ b/tools/rename-bins
@@ -0,0 +1,5 @@
+#!/bin/sh -e
+
+while read old new html ; do
+  mv -f "./$old" "./$new"
+done < ./tools/name-table