-echo " Target: $target"
-echo " Prefix: $prefix"
-echo " Data Directory: $DATADIR"
-echo " Log Level: $log_level"
-echo " Debug: $debug"
-echo " Profile: $profile"
-echo " Extra Warnings: $extra_warnings"
+echo " Target: $target"
+echo " Prefix: $prefix"
+echo " Data Directory: $DATADIR"
+echo " Log Level: $log_level"
+echo " Debug: $debug"
+echo " Double Precision: $double_precision"
+echo " Profile: $profile"
+echo " Extra Warnings: $extra_warnings"