diff options
author | Michael Schmidt <github@mschmidt.me> | 2015-11-06 13:04:58 +0100 |
---|---|---|
committer | Michael Schmidt <github@mschmidt.me> | 2015-11-06 13:04:58 +0100 |
commit | 31fcfe29ebf1ef6eea487e8ce18eb5e11fb60b67 (patch) | |
tree | b5a2012cf3143c7a2ee1a8da9da98c2e2a7e1cb2 /debug/DebugTypes.mli | |
parent | e5aeeb137cfd95289ec9388318f65df6f5b08db6 (diff) | |
download | compcert-kvx-31fcfe29ebf1ef6eea487e8ce18eb5e11fb60b67.tar.gz compcert-kvx-31fcfe29ebf1ef6eea487e8ce18eb5e11fb60b67.zip |
bug 17567, typos
Diffstat (limited to 'debug/DebugTypes.mli')
-rw-r--r-- | debug/DebugTypes.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/debug/DebugTypes.mli b/debug/DebugTypes.mli index b2f19f7a..e885fc59 100644 --- a/debug/DebugTypes.mli +++ b/debug/DebugTypes.mli @@ -147,7 +147,7 @@ type local_variable_information = { lvar_atom: atom option; lvar_file_loc:location; lvar_type: int; - lvar_static: bool; (* Static variable are mapped to symbols *) + lvar_static: bool; (* Static variables are mapped to symbols *) } type scope_information = |