diff options
| -rw-r--r-- | MAINTAINERS | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/MAINTAINERS b/MAINTAINERS index 3615f3c266..438ae492bf 100644 --- a/MAINTAINERS +++ b/MAINTAINERS @@ -213,6 +213,11 @@ M: Stefano Stabellini <stefano.stabellini@eu.citrix.com> S: Supported F: extras/mini-os/ +OCAML TOOLS +M: David Scott <dave.scott@eu.citrix.com> +S: Supported +F: tools/ocaml/ + QEMU-DM M: Ian Jackson <ian.jackson@eu.citrix.com> S: Supported |