diff options
Diffstat (limited to 'src/ast_util.ml')
| -rw-r--r-- | src/ast_util.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 158b40a8..548cd15e 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -1714,6 +1714,15 @@ let unique l = incr unique_ref; l +let extern_assoc backend exts = + try + try + Some (List.assoc backend exts) + with Not_found -> + Some (List.assoc "_" exts) + with Not_found -> + None + (**************************************************************************) (* 1. Substitutions *) (**************************************************************************) |
