From b4e285f91ac233916ae309d1bd2099257dcc57f4 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Thu, 2 Jan 2020 08:33:33 -0500 Subject: [PATCH] fix: dead link in doc --- doc/make/index.md | 1 - 1 file changed, 1 deletion(-) diff --git a/doc/make/index.md b/doc/make/index.md index 54e6dd1606..05e7ee8fbd 100644 --- a/doc/make/index.md +++ b/doc/make/index.md @@ -111,6 +111,5 @@ Troubleshooting Further Information ------------------- -- [Using CCache](ccache.md) to avoid recompilation - [Measuring Code Coverage](coverage.md) - [Compiling Lean with Split Stacks](split-stack.md)