tools/build_all_headers.py exception - broken by rp2040 and rp2350 duplicate file names

[d-c-d]

in the top level pico-sdk folder

$ python3 tools/build_all_headers.py  $PWD /tmp/build_all_headers.out
Traceback (most recent call last):
  File "/cygdrive/c/git/pico-sdk/tools/build_all_headers.py", line 66, in <module>
    raise Exception("Duplicate include file '{}' (found in both {} and {})".format(include_file, include_locations[include_file], include_path))
Exception: Duplicate include file 'boot_stage2/config.h' (found in both rp2040/boot_stage2/include and rp2350/boot_stage2/include)

workaround - add IGNORE_DIRS.add('rp2040') or IGNORE_DIRS.add('rp2350')

While useful, there were no examples of this tool being used.

[lurch]

It's something I added a long time ago in #319 - it's not really something that we expected anybody to actually use for anything 😂

[d-c-d]

For context, I only ran into the file tools/build_all_headers.py because I was trying to see if semihosting would be valuable in my debug context, so I was looking at all ( of the few places semihosting was mentioned :-) )

[d-c-d]

I'm guessing a milestone of none indicates a won't fix, is that correct?
What about deleting the file then?

[lurch]

See #2292

[lurch]

Fixed in develop