Mike wrote me separately to say the problem eventually fixed itself for
no evident reason :(. Maybe related to our general timing issue?
Anyway, closing. --thanks, karl.
On Sat, 9 Dec 2023 at 15:16, Reuben Thomas wrote:
>
> If you're happy with that, I'll write a patch.
>
Patch attached.
--
https://rrt.sc3d.org
From 06f6765b7d10132d0dcefde1265b4d5f01df76b4 Mon Sep 17 00:00:00 2001
From: Reuben Thomas
Date: Sat, 9 Dec 2023 15:20:44 +0200
Subject: [PATCH] doc:
On Sat, 9 Dec 2023 at 00:03, Karl Berry wrote:
> The manual currently says: "You should never explicitly mention the
> intermediate (C or C++) file in any `SOURCES' variable; only list
> the source file."
>
> I don't know the code here, and this probably wasn't the question, but I
>