diff options
Diffstat (limited to 'docs/mono-tools.source')
-rw-r--r-- | docs/mono-tools.source | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/docs/mono-tools.source b/docs/mono-tools.source new file mode 100644 index 00000000000..e545ef17a84 --- /dev/null +++ b/docs/mono-tools.source @@ -0,0 +1,5 @@ +<?xml version="1.0"?> +<monodoc> + <node label="Mono Development Tools" name="dev-tools" parent="tools" /> + <source provider="man" basefile="mono-tools" path="dev-tools"/> +</monodoc> |