diff options
| author | Michael Schmidt <github@mschmidt.me> | 2015-10-14 15:07:48 +0200 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2015-10-14 15:07:48 +0200 |
| commit | 60ab550a952c3d9719b2a91ec90c9b58769f6717 (patch) | |
| tree | 523cf4eb5a35594b16a297b4bd7e29157f42b0fc /common/Sections.ml | |
| parent | a479c280441b91007c379b0b63b907926d54f930 (diff) | |
| download | compcert-kvx-60ab550a952c3d9719b2a91ec90c9b58769f6717.tar.gz compcert-kvx-60ab550a952c3d9719b2a91ec90c9b58769f6717.zip | |
bug 17392: remove trailing whitespace in source files
Diffstat (limited to 'common/Sections.ml')
| -rw-r--r-- | common/Sections.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/common/Sections.ml b/common/Sections.ml index 0910f2dc..93783155 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -58,7 +58,7 @@ let default_section_info = { let builtin_sections = [ "CODE", - {sec_name_init = Section_text; + {sec_name_init = Section_text; sec_name_uninit = Section_text; sec_writable = false; sec_executable = true; sec_access = Access_default}; @@ -119,7 +119,7 @@ let initialize () = (* Define or update a given section. *) let define_section name ?iname ?uname ?writable ?executable ?access () = - let si = + let si = try Hashtbl.find current_section_table name with Not_found -> default_section_info in let writable = @@ -218,7 +218,7 @@ let for_function env id ty_res = with Not_found -> assert false in [si_code.sec_name_init; si_literal.sec_name_init; si_jumptbl.sec_name_init] - + (* Determine section for a string literal *) let for_stringlit() = |