On Wed, Nov 12, 2025 at 01:25:57PM +0000, David Laight wrote: > On Wed, 12 Nov 2025 04:32:02 +0000 Michael Kelley <[email protected]> > wrote: > > From: Josh Poimboeuf <[email protected]> Sent: Tuesday, November 11, 2025 > > 8:04 PM > > > On Wed, Nov 12, 2025 at 02:26:18AM +0000, Michael Kelley wrote: > > > > > 2) With make v4.2.1 on my Ubuntu 20.04 system, the "#" character in > > > > > the > > > > > "#include" added to the echo command is problematic. "make" seems to > > > > > be > > > > > treating it as a comment character, though I'm not 100% sure of that > > > > > interpretation. Regardless, the "#" causes a syntax error in the > > > > > "make" shell > > > > > command. Adding a backslash before the "#" solves that problem. On an > > > > > Ubuntu > > > > > 24.04 system with make v4.3, the "#" does not cause any problems. (I > > > > > tried to put > > > > > make 4.3 on my Ubuntu 20.04 system, but ran into library > > > > > compatibility problems > > > > > so I wasn’t able to definitively confirm that it is the make version > > > > > that changes the > > > > > handling of the "#"). Unfortunately, adding the backslash before the > > > > > # does *not* > > > > > work with make v4.3. The backslash becomes part of the C source code > > > > > sent to > > > > > gcc, which barfs. I don't immediately have a suggestion on how to > > > > > resolve this > > > > > in a way that is compatible across make versions. > > > > > > > > Using "\043" instead of the "#" is a compatible solution that works in > > > > make > > > > v4.2.1 and v4.3 and presumably all other versions as well. > > > > > > Hm... I've seen similar portability issues with "," for which we had to > > > change it to "$(comma)" which magically worked for some reason that I am > > > forgetting. > > > > > > Does "$(pound)" work? This seems to work here: > > Please not 'pound' - that is the uk currency symbol (not what US greengrocers > scrawl for lb).
While I do call it the "pound sign", I can't take the credit/blame for that name it as the variable already exists. It's better than "hashtag" which is what my kids call it :-/ -- Josh
