summaryrefslogtreecommitdiff
path: root/src/process_file.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2019-07-18 18:36:52 +0100
committerAlasdair Armstrong2019-07-18 18:36:52 +0100
commit3bf4b4489f4e8ee114773802bfc9d5a4a9e13d0b (patch)
tree63b8ba850de64ba3f4a58b854883022ddb4ef376 /src/process_file.ml
parentdf325dfefda5d7ffbfd3870c2af0378cb3862e07 (diff)
Add a option to check for a feature symbol
Diffstat (limited to 'src/process_file.ml')
-rw-r--r--src/process_file.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/process_file.ml b/src/process_file.ml
index 170a544a..d239b0c0 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -99,6 +99,9 @@ let default_symbols =
let symbols = ref default_symbols
+let have_symbol symbol =
+ StringSet.mem symbol !symbols
+
let clear_symbols () = symbols := default_symbols
let cond_pragma l defs =