add float to user data

This commit is contained in:
Simon Cruanes 2023-09-04 22:51:11 -04:00
parent 431811c995
commit aafe2e5187
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4

View file

@ -7,6 +7,7 @@ type user_data =
[ `Int of int
| `String of string
| `Bool of bool
| `Float of float
| `None
]
(** User defined data, generally passed as key/value pairs to