diff --git a/maintenance/dummytool.c b/maintenance/dummytool.c
deleted file mode 100644
index 0566948a6..000000000
--- a/maintenance/dummytool.c
+++ /dev/null
@@ -1,7 +0,0 @@
-// Note: do not remove, used by ../configure
-
-#include <stdio.h>
-
-int main(int argc, char **argv) {
-  return 0;
-}