aboutsummaryrefslogtreecommitdiffstats
path: root/common/Sections.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-03-11 18:02:36 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-03-11 18:02:36 +0100
commita84576b219c797467e480508fc99ba78260062df (patch)
tree8b7d42d170270bb9a7a53be00c63d60591113f9c /common/Sections.ml
parenta6924f1a53c1ab2edeb4df4833cbc341e4f2d256 (diff)
downloadcompcert-kvx-a84576b219c797467e480508fc99ba78260062df.tar.gz
compcert-kvx-a84576b219c797467e480508fc99ba78260062df.zip
Started integrating the debug printing in the common backend_printer.
Diffstat (limited to 'common/Sections.ml')
-rw-r--r--common/Sections.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/common/Sections.ml b/common/Sections.ml
index 086c860e..c0c95848 100644
--- a/common/Sections.ml
+++ b/common/Sections.ml
@@ -27,7 +27,7 @@ type section_name =
| Section_literal
| Section_jumptable
| Section_user of string * bool (*writable*) * bool (*executable*)
- | Section_debug
+ | Section_debug_info
| Section_debug_abbrev
type access_mode =