diff options
| author | Brian Campbell | 2020-08-27 13:54:24 +0100 |
|---|---|---|
| committer | Brian Campbell | 2020-08-27 13:54:24 +0100 |
| commit | c16e6137e954e9a4cd24fb81dbafcfef27206837 (patch) | |
| tree | f0a90051c8b88b8216ecad613fa81c8f9c81ad9c /src | |
| parent | 005990f1726719fa7d9f8f2d56fe8aaa7128f376 (diff) | |
Ignore file start/end pragmas in splice
Diffstat (limited to 'src')
| -rw-r--r-- | src/splice.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/splice.ml b/src/splice.ml index 8ebd5793..dd19e664 100644 --- a/src/splice.ml +++ b/src/splice.ml @@ -12,6 +12,8 @@ let scan_defs (Defs defs) = IdSet.add (id_of_fundef fd) ids, specs | DEF_spec (VS_aux (VS_val_spec (_,id,_,_),_) as vs) -> ids, Bindings.add id vs specs + | DEF_pragma (("file_start" | "file_end"), _ ,_) -> + ids, specs | d -> raise (Reporting.err_general (def_loc d) "Definition in splice file isn't a spec or function") in List.fold_left scan (IdSet.empty, Bindings.empty) defs |