diff options
Diffstat (limited to 'www/geneweb/files/patch-ged2gwb_ged2gwb2.ml')
| -rw-r--r-- | www/geneweb/files/patch-ged2gwb_ged2gwb2.ml | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/www/geneweb/files/patch-ged2gwb_ged2gwb2.ml b/www/geneweb/files/patch-ged2gwb_ged2gwb2.ml new file mode 100644 index 000000000000..dfd4eb15e342 --- /dev/null +++ b/www/geneweb/files/patch-ged2gwb_ged2gwb2.ml @@ -0,0 +1,11 @@ +--- ged2gwb/ged2gwb2.ml.orig 2024-02-11 19:44:49 UTC ++++ ged2gwb/ged2gwb2.ml +@@ -501,7 +501,7 @@ value date_lexer = + ; + + value date_lexer = +- {Token.tok_func s = (make_date_lexing s, fun _ -> Token.dummy_loc); ++ {Token.tok_func s = (make_date_lexing s, Plexing.Locations.create ()); + Token.tok_using = using_token; Token.tok_removing _ = (); + Token.tok_match = tparse; Token.tok_text _ = "<tok>"; + Token.tok_comm = None} |