chore: fix leanc.sh -v

leanprover · Nov 9, 2021 · b36e253 · b36e253
1 parent d9e4111
commit b36e253
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/bin/leanc.in b/src/bin/leanc.in
@@ -9,5 +9,5 @@ for arg in "$@"; do
 done
 cmd=(${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_FLAGS@ @LEANC_INTERNAL_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument)
 cmd=$(printf '%q ' "${cmd[@]}" | sed "s!ROOT!$root!g")
-[[ $v == 1 ]] && printf '%q ' $cmd
+[[ $v == 1 ]] && echo $cmd
 eval $cmd