GitLab

48cf32db

by Zubin Duggal at 2025-07-02T18:25:57+05:30

fetch_gitlab: Ensure we copy users_guide.pdf and Haddock.pdf to the release docs directory

Fixes #24093

@@ -134,6 +134,9 @@ def fetch_artifacts(release: str, pipeline_id: int,
                      logging.info(f'extracted docs {f} to {dest}')
                  index_path = destdir / 'docs' / 'index.html'
                  index_path.replace(dest / 'index.html')
 +                pdfs = list(destdir.glob('*.pdf'))
 +                for f in pdfs:
 +                  f.replace(dest / f.name)
              elif job.name == 'hackage-doc-tarball':
                  dest = dest_dir / 'hackage_docs'
                  logging.info(f'moved hackage_docs to {dest}')