1 files changed, 4 insertions, 0 deletions
diff --git a/tools/cover.pl b/tools/cover.pl
index 379a17e..c2ac5d0 100755
--- a/tools/cover.pl
+++ b/tools/cover.pl
@@ -58,3 +58,7 @@ foreach my $build_dir (glob("cover_db/$build.*/")) {
 }
 
 system 'cover', '-write', "cover_db/$build", glob("cover_db/$build.*/cover_db/");
+
+my $output = shift // "cover_db/$build";
+
+system 'cover', '-outputdir', $output;