aboutsummaryrefslogtreecommitdiffstats
path: root/common/Sections.mli
diff options
context:
space:
mode:
Diffstat (limited to 'common/Sections.mli')
-rw-r--r--common/Sections.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/common/Sections.mli b/common/Sections.mli
index b83b0bb4..bc97814d 100644
--- a/common/Sections.mli
+++ b/common/Sections.mli
@@ -32,6 +32,7 @@ type section_name =
| Section_debug_line of string option
| Section_debug_ranges
| Section_debug_str
+ | Section_ais_annotation
type access_mode =
| Access_default