diff --git a/misc-scripts/xref_mapping/xref_parser.pl b/misc-scripts/xref_mapping/xref_parser.pl index 452ceccc01bb59f302c07b8637da72571c9e29ee..f2cb661bd4188a9421637cf92ecc3d83ea76c8c4 100644 --- a/misc-scripts/xref_mapping/xref_parser.pl +++ b/misc-scripts/xref_mapping/xref_parser.pl @@ -10,6 +10,8 @@ my ( $host, $port, $dbname, $deletedownloaded, $dl_path, @notsource, $unzip, $stats ); +print "Options: ".join(" ",@ARGV)."\n"; + $unzip = 0; # Do not decompress gzipped files by default GetOptions(