diff options
| author | Alasdair Armstrong | 2019-07-18 18:36:52 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-07-18 18:36:52 +0100 |
| commit | 3bf4b4489f4e8ee114773802bfc9d5a4a9e13d0b (patch) | |
| tree | 63b8ba850de64ba3f4a58b854883022ddb4ef376 /src/process_file.ml | |
| parent | df325dfefda5d7ffbfd3870c2af0378cb3862e07 (diff) | |
Add a option to check for a feature symbol
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 3 |
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 = |
