Merge branch 'releases/gcc-13' into devel/omp/gcc-13

Merge up to r13-7985-g319e887bdddfb8b9244f9310a54c1f08b7e8f0e8 (26th Oct 2023)

diff --cc gcc/c-family/c-pragma.cc
Simple merge

diff --cc gcc/doc/extend.texi
Simple merge

diff --cc gcc/opts.cc
Simple merge