diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index aee37305c..e3b09f3c9 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -289,6 +289,16 @@ let print_inline_asm print_preg oc txt sg args res =
   List.iter print_fragment (Str.full_split re_asm_param_1 txt);
   fprintf oc "\n"
 
+(** Print command-line argument, with quoting if needed.
+    We quote using double quotes if the argument contains whitespace,
+    control characters, or double quotes. *)
+
+let re_unquoted = Str.regexp "[^ \x00-\x1F\"]*$"
+
+let quote_argument s =
+  if Str.string_match re_unquoted s 0
+  then s
+  else "\"" ^ String.escaped s ^ "\""
 
 (** Print CompCert version and command-line as asm comment *)
 
@@ -301,7 +311,7 @@ let print_version_and_options oc comment =
   fprintf oc "%s File generated by CompCert %s\n" comment version_string;
   fprintf oc "%s Command line:" comment;
   for i = 1 to Array.length Commandline.argv - 1 do
-    fprintf oc " %s" Commandline.argv.(i)
+    fprintf oc " %s" (quote_argument Commandline.argv.(i))
   done;
   fprintf oc "\n"