From 5933cd8205a3c4b358435736c4b7a83f8f033473 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 18 Sep 2023 17:35:52 -0400
Subject: [PATCH 1/2] create etc/emacs/run-etags.sh to make argument processing
 clear

---
 Makefile.coq.local     | 4 +---
 dune                   | 8 +++++---
 etc/emacs/etags-args   | 2 --
 etc/emacs/run-etags.sh | 2 ++
 4 files changed, 8 insertions(+), 8 deletions(-)
 delete mode 100644 etc/emacs/etags-args
 create mode 100755 etc/emacs/run-etags.sh

diff --git a/Makefile.coq.local b/Makefile.coq.local
index 0635dd131ce..4f167cf518e 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -31,8 +31,6 @@ ALECTRYON_EXTRAFLAGS ?=
 # setting TIMING=1. By doing so here we get the same effect.
 TIMING ?= 1
 
-ETAGS ?= etags
-
 CATEGORY_VFILES = $(filter theories/Categories%.v, $(VFILES))
 CORE_VFILES = $(filter-out $(CATEGORY_VFILES),$(filter theories/%.v, $(VFILES)))
 CONTRIB_VFILES = $(filter contrib/%.v, $(VFILES))
@@ -242,7 +240,7 @@ dot-file-dep-graphs: $(ALL_DOTFILES)
 # The TAGS file
 TAGS_FILES = $(ALL_VFILES)
 TAGS : $(TAGS_FILES)
-	$(ETAGS) --language=none $(shell cat etc/emacs/etags-args) $^
+	./etc/emacs/run-etags.sh $^
 
 # We separate things to work around `make: execvp: /bin/bash: Argument list too long`
 clean::
diff --git a/dune b/dune
index 0de0fb730de..fc1ae51c00a 100644
--- a/dune
+++ b/dune
@@ -55,7 +55,9 @@
  (alias emacs)
  (mode promote)
  (deps
-  %{bin:etags}
-  (glob_files_rec ./*.v))
+  etc/emacs/run-etags.sh
+  (:vfile
+   (glob_files_rec theories/*.v)
+   (glob_files_rec contrib/*.v)))
  (action
-  (run etags --language=none %{read:etc/emacs/etags-args} %{deps})))
+  (run etc/emacs/run-etags.sh %{vfile})))
diff --git a/etc/emacs/etags-args b/etc/emacs/etags-args
deleted file mode 100644
index c4b9dbd7fad..00000000000
--- a/etc/emacs/etags-args
+++ /dev/null
@@ -1,2 +0,0 @@
--r '/^[ \t]*\(\(Local\|Global\|Cumulative\|NonCumulative\|Monomorphic\|Polymorphic\|Private\)[ \t]+\)*\(Axiom\|Theorem\|Class\|Instance\|Let\|Ltac\|Definition\|Lemma\|Record\|Remark\|Structure\|Fixpoint\|Fact\|Corollary\|Inductive\|CoInductive\|Proposition\)[ \t]+\([a-zA-Z0-9_'\'']+\)/\4/' 
--r '/^[ \t]*\([a-zA-Z0-9_'\'']+\)[ \t]*:/\1/' 
\ No newline at end of file
diff --git a/etc/emacs/run-etags.sh b/etc/emacs/run-etags.sh
new file mode 100755
index 00000000000..b693697b490
--- /dev/null
+++ b/etc/emacs/run-etags.sh
@@ -0,0 +1,2 @@
+#!/bin/sh
+etags --language=none -r '/^[ \t]*\(\(Local\|Global\|Cumulative\|NonCumulative\|Monomorphic\|Polymorphic\|Private\)[ \t]+\)*\(Axiom\|Theorem\|Class\|Instance\|Let\|Ltac\|Definition\|Lemma\|Record\|Remark\|Structure\|Fixpoint\|Fact\|Corollary\|Inductive\|CoInductive\|Proposition\)[ \t]+\([a-zA-Z0-9_'\'']+\)/\4/' -r '/^[ \t]*\([a-zA-Z0-9_'\'']+\)[ \t]*:/\1/' "$@"

From fded172afcc8c4e047335f551e209a90d6cdce06 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 18 Sep 2023 17:48:16 -0400
Subject: [PATCH 2/2] dune: keep etags as a dependency of the TAGS target

---
 dune | 1 +
 1 file changed, 1 insertion(+)

diff --git a/dune b/dune
index fc1ae51c00a..70098e32031 100644
--- a/dune
+++ b/dune
@@ -56,6 +56,7 @@
  (mode promote)
  (deps
   etc/emacs/run-etags.sh
+  %{bin:etags}
   (:vfile
    (glob_files_rec theories/*.v)
    (glob_files_rec contrib/*.v)))