From d0be25cd8848c9bcb6f5e8a59d46271e96bed09c Mon Sep 17 00:00:00 2001 From: Jeremie Dimino Date: Mon, 15 May 2017 17:14:10 +0100 Subject: [PATCH] manual.org and quick-start.org no longer exist --- doc/jbuild | 4 ---- 1 file changed, 4 deletions(-) diff --git a/doc/jbuild b/doc/jbuild index a863b6ae..e4cf1f24 100644 --- a/doc/jbuild +++ b/doc/jbuild @@ -18,10 +18,6 @@ let jbuild = ({| (jbuild_version 1) -(install - ((section doc) - (files (manual.org quick-start.org)))) - (rule ((targets (jbuilder.1)) (action (with-stdout-to ${@}