Make script work from any directory

martinescardo · Jul 17, 2024 · f06ef9b · f06ef9b
1 parent 190c2d8
commit f06ef9b
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/count-agda-files-and-lines b/count-agda-files-and-lines
@@ -1,2 +1,6 @@
-git ls-files source |  grep agda | wc -l
-git ls-files source | grep agda | xargs cat | wc -l
+#!/bin/bash
+
+ROOT_DIR=$(git rev-parse --show-toplevel)
+
+git ls-files $ROOT_DIR/source | grep agda | wc -l
+git ls-files $ROOT_DIR/source | grep agda | xargs cat | wc -l