diff --git a/build/patchdef.cpp b/build/patchdef.cpp
deleted file mode 100644
index 1c2b15dd8..000000000
--- a/build/patchdef.cpp
+++ /dev/null
@@ -1,51 +0,0 @@
-#include <ctype.h>
-#include <string.h>
-#include <fstream.h>
-
-
-void patch(istream& i, ostream& o)
-{
-  char lin[513];
-
-  while (i.good())
-  {
-    i.getline(lin, 512);
-
-    for(char* c = lin; isspace(*c); c++);  // salta spazi iniziali
-
-    char instring = '\0';
-    char wasspace = 0;
-
-    for (char* cur = lin; *c; c++)
-    {
-      if (*c == '!')
-      {
-        if (*(c + 1) == '!')
-        {
-          c++;
-          *c = '#';
-        }
-      }
-      if (*c == '#')
-      {
-        *cur++ = *c;
-        while isspace(*(++c));
-      }
-      if (*c == ';')
-       *cur++ = '\n';
-      else
-       *cur++ = *c;
-    }
-    *cur = '\0';
-
-    if (*lin) o << lin << endl;
-  }
-}
-
-
-int main()
-{
-  patch(cin, cout);
-  return 0;
-}
-
\ No newline at end of file