fix paths in checktodos.sh

MetaCoq · Jan 16, 2023 · 7196e19 · 7196e19
1 parent 0d7b23d
commit 7196e19
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/checktodos.sh b/checktodos.sh
@@ -1,6 +1,6 @@
 #!/bin/bash
 
-if [[ $(git grep -c todo | grep theories) = template-coq/theories/utils/MCUtils.v:3 ]]
+if [[ $(git grep -c todo | grep theories) = utils/theories/MCUtils.v:3 ]]
 then
     echo "No todos found"
     if [[ $(git grep -c Admitted | grep theories) = "" ]]
@@ -14,7 +14,7 @@ then
     fi
 else
     echo "Found todos:"
-    git grep -c todo | grep theories | grep -v "template-coq/theories/utils/MCUtils.v:3"
+    git grep -c todo | grep theories | grep -v "utils/theories/MCUtils.v:3"
     exit 1
 fi
 endef