summaryrefslogtreecommitdiff
path: root/src/process_file.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/process_file.ml')
-rw-r--r--src/process_file.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/process_file.ml b/src/process_file.ml
index d2a86595..116788b9 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -108,6 +108,8 @@ let have_symbol symbol =
let clear_symbols () = symbols := default_symbols
+let add_symbol str = symbols := StringSet.add str !symbols
+
let cond_pragma l defs =
let depth = ref 0 in
let in_then = ref true in