From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Wed, 13 Jan 2021 01:56:12 +0000 (+0000)
Subject: Makefile: drop "doc" from default build
X-Git-Tag: otter-0.3.0~35
X-Git-Url: https://www.chiark.greenend.org.uk/ucgi/~ianmdlvl/git?a=commitdiff_plain;h=c8abe31798b07319a20abffc1e98ee21cec8c8ae;p=otter.git

Makefile: drop "doc" from default build

It is slow and annoying

Signed-off-by: Ian Jackson <ijackson@chiark.greenend.org.uk>
---

diff --git a/Makefile b/Makefile
index 651eb073..9222a8d6 100644
--- a/Makefile
+++ b/Makefile
@@ -10,7 +10,7 @@
 SHELL=/bin/bash
 src=.
 
-default: all check doc
+default: all check
 all: debug
 everything: debug doc release check bundled-sources