Remove developer docs

They're essentially useless.
2019-05-04 12:28:24 -03:00
parent f55b4531ef
commit 682e614e4b
26 changed files with 1 additions and 4921 deletions
@@ -159,8 +159,7 @@
                }
            ],
            "config-opts" : [
-                "-Dtracing=true",
-                "-Ddocumentation=true"
+                "-Dtracing=true"
            ]
        }
    ]