From 503256c6bd04cb6bdf2142d3bc12a56461e9ce52 Mon Sep 17 00:00:00 2001 From: Gareth Rees Date: Sun, 23 Aug 2020 15:47:50 +0100 Subject: [PATCH] Avoid "unknown target name" warning when building the manual. --- mps/design/writef.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/mps/design/writef.txt b/mps/design/writef.txt index de01db09011..86f84d04a52 100644 --- a/mps/design/writef.txt +++ b/mps/design/writef.txt @@ -145,6 +145,7 @@ particular type ``void (*)(void)`` is chosen because in GCC from ``-Wcast-function-type``. See job004156_ and `GCC Warning Options`_. +.. _job004156: https://www.ravenbrook.com/project/mps/issue/job004156/ .. _GCC Warning Options: https://gcc.gnu.org/onlinedocs/gcc/Warning-Options.html