Set dynamic users-guide TOC spacing (fixes #18554)

24 jobs for !4499 with userguide-pdf-toc-spacing in 394 minutes and 56 seconds (queued for 1 second)
latest merge request
Name Stage Failure
failed
validate-armv7-linux-deb10 Full Build
Uploading artifacts...
WARNING: ghc-armv7-linux-deb10.tar.xz: no matching files
WARNING: junit.xml: no matching files
WARNING: performance-metrics.tsv: no matching files
ERROR: No files to upload
Uploading artifacts...
WARNING: junit.xml: no matching files
ERROR: No files to upload
ERROR: Job failed: exit code 1
failed
validate-aarch64-linux-deb10 Full Build
Uploading artifacts...
WARNING: ghc-aarch64-linux-deb10.tar.xz: no matching files
WARNING: junit.xml: no matching files
WARNING: performance-metrics.tsv: no matching files
ERROR: No files to upload
Uploading artifacts...
WARNING: junit.xml: no matching files
ERROR: No files to upload
ERROR: Job failed: exit code 1
failed
doc-tarball Packaging
+ cd ..
+ '[' 0 -eq 0 ']'
+ rm -r linux
+ tar -Jxf /builds/timbobbarnes/ghc/ghc-x86_64-unknown-mingw32.tar.xz
+ mv ghc-9.1.0.20201123-x86_64-unknown-mingw32 windows
+ cd inst/share/doc/ghc-9.1.0.20201123/html/libraries
+ mv '../../../../../../windows/doc/html/libraries/Win32-*' .
mv: cannot stat '../../../../../../windows/doc/html/libraries/Win32-*': No such file or directory
ERROR: Job failed: exit code 1