diff options
Diffstat (limited to 'ia32')
| -rw-r--r-- | ia32/PrintAsm.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 01034f1..79da85e 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -873,6 +873,7 @@ let print_globdef oc (name, gdef) = | Gvar v -> print_var oc name v let print_program oc p = + PrintAnnot.print_version_and_options oc comment; need_masks := false; indirect_symbols := StringSet.empty; Hashtbl.clear filename_num; |