From 431541f91a09e9d8fe3b027475975a771d93332a Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sun, 29 Mar 2020 22:12:47 +0200
Subject: [dune] [docgram] Remove bash hack thanks to new option -no-update.

---
 doc/tools/docgram/dune | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune
index fba4856241..a533a6d367 100644
--- a/doc/tools/docgram/dune
+++ b/doc/tools/docgram/dune
@@ -43,9 +43,6 @@
   orderedGrammar)
  (action
   (progn
-   (bash "for f in fullGrammar orderedGrammar; do cp ${f} ${f}.old; done")
-   (chdir %{project_root} (run doc_grammar -check-cmds %{input}))
-   (bash "for f in fullGrammar orderedGrammar; do cp ${f} ${f}.new; done")
-   (bash "for f in fullGrammar orderedGrammar; do cp ${f}.old ${f}; done")
+   (chdir %{project_root} (run doc_grammar -check-cmds -no-update %{input}))
    (diff? fullGrammar fullGrammar.new)
    (diff? orderedGrammar orderedGrammar.new))))
-- 
cgit v1.2.3