aboutsummaryrefslogtreecommitdiffstats
path: root/community/ocaml/fix-check-parser-uptodate-or-warn.sh.patch
diff options
context:
space:
mode:
Diffstat (limited to 'community/ocaml/fix-check-parser-uptodate-or-warn.sh.patch')
-rw-r--r--community/ocaml/fix-check-parser-uptodate-or-warn.sh.patch14
1 files changed, 0 insertions, 14 deletions
diff --git a/community/ocaml/fix-check-parser-uptodate-or-warn.sh.patch b/community/ocaml/fix-check-parser-uptodate-or-warn.sh.patch
deleted file mode 100644
index f78aaf0c238..00000000000
--- a/community/ocaml/fix-check-parser-uptodate-or-warn.sh.patch
+++ /dev/null
@@ -1,14 +0,0 @@
---- a/tools/check-parser-uptodate-or-warn.sh 2019-06-14 08:21:51.000000000 -0300
-+++ b/tools/check-parser-uptodate-or-warn.sh 2019-07-16 14:56:27.352376332 -0300
-@@ -43,8 +43,8 @@
- }
-
- # The check itself
--SOURCE_MTIME=$(mtime parsing/parser.mly)
--GENERATED_MTIME=$(mtime boot/menhir/parser.ml)
-+SOURCE_MTIME=$(mtime "$builddir"/parsing/parser.mly)
-+GENERATED_MTIME=$(mtime "$builddir"/boot/menhir/parser.ml)
- if test $SOURCE_MTIME -gt $(( $GENERATED_MTIME + 10 ))
- then
- echo
-