diff options
Diffstat (limited to 'tools/cleanup-header')
| -rw-r--r-- | tools/cleanup-header | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/tools/cleanup-header b/tools/cleanup-header deleted file mode 100644 index 9c2147573c..0000000000 --- a/tools/cleanup-header +++ /dev/null @@ -1,15 +0,0 @@ -#!/bin/sed -f -# Remove private parts from runtime include files, before installation -# in /usr/local/lib/ocaml/caml - -/\/\* <include \.\.\/config\/m\.h> \*\// { - r ../config/m.h - d -} -/\/\* <include \.\.\/config\/s\.h> \*\// { - r ../config/s.h - d -} -/\/\* <private> \*\//,/\/\* <\/private> \*\//d - - |