diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp
index db33ac5b194..0804dacdd6d 100644
--- a/src/goto-cc/gcc_mode.cpp
+++ b/src/goto-cc/gcc_mode.cpp
@@ -1022,6 +1022,9 @@ int gcc_modet::asm_output(
       output_files.begin()->second=="/dev/null"))
     return EX_OK;
 
+  #if 0
+  // The below disturbs some scripts that rummage through assembly
+  // output.
   debug()
     << "Appending preprocessed sources to generate hybrid asm output"
     << eom;
@@ -1053,6 +1056,7 @@ int gcc_modet::asm_output(
       os << comment << comment << line << '\n';
     }
   }
+  #endif
 
   return EX_OK;
 }