aboutsummaryrefslogtreecommitdiffstats
path: root/debug/DwarfTypes.mli
diff options
context:
space:
mode:
authorMichael Schmidt <github@mschmidt.me>2015-10-14 15:07:48 +0200
committerMichael Schmidt <github@mschmidt.me>2015-10-14 15:07:48 +0200
commit60ab550a952c3d9719b2a91ec90c9b58769f6717 (patch)
tree523cf4eb5a35594b16a297b4bd7e29157f42b0fc /debug/DwarfTypes.mli
parenta479c280441b91007c379b0b63b907926d54f930 (diff)
downloadcompcert-kvx-60ab550a952c3d9719b2a91ec90c9b58769f6717.tar.gz
compcert-kvx-60ab550a952c3d9719b2a91ec90c9b58769f6717.zip
bug 17392: remove trailing whitespace in source files
Diffstat (limited to 'debug/DwarfTypes.mli')
-rw-r--r--debug/DwarfTypes.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli
index c7e5dce1..7048d8d3 100644
--- a/debug/DwarfTypes.mli
+++ b/debug/DwarfTypes.mli
@@ -47,7 +47,7 @@ type location_value =
| LocRef of address
| LocSimple of location_expression
| LocList of location_expression list
-
+
type data_location_value =
| DataLocBlock of location_expression
| DataLocRef of reference
@@ -62,10 +62,10 @@ type string_const =
(* Types representing the attribute information per tag value *)
-type file_loc =
+type file_loc =
| Diab_file_loc of constant * constant
| Gnu_file_loc of constant * constant
-
+
type dw_tag_array_type =
{
array_type: reference;