Fix missing '$'

GaloisInc · Jul 14, 2023 · ae23bdc · ae23bdc
1 parent 1af0efa
commit ae23bdc
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/.github/ci.sh b/.github/ci.sh
@@ -157,7 +157,7 @@ files_since() {
 compute_coverage() {
   # Combine .tix files
   local SUM_TIX="all.tix"
-  hpc sum --output=$SUM_TIX --union --exclude=Main --exclude=GitRev (find . -name "*.tix")
+  hpc sum --output=$SUM_TIX --union --exclude=Main --exclude=GitRev $(find . -name "*.tix")
   # Generate report
   local HPC_ROOT=$(find dist-newstyle -name "hpc")
   # TODO: Remove debug echos"