Skip to content

Change important CI DOS batch files to CRLF #8610

@MSoegtropIMC

Description

@MSoegtropIMC

Currently all Windows batch files used on CI use LF line endings. Unfortunately this can have the effect that jump/call labels are not found (but only if the jump label is more than 512 bytes away from the call and the moon is in a certain constellation to Saturn, otherwise it works fine - oh how we love MS). So I fear I have to change some important CI batch files to CRLF, although this makes diffing hard.

See https://web.archive.org/web/20160305063042/help.wugnet.com/windows/system-find-batch-label-ftopict615555.html

I actually run into this issue in CI job

https://gitlab.com/coq/coq/-/jobs/103241210

At the end it complains "The system cannot find the batch label specified - CopyLogFiles", but the label is definitely there.

Metadata

Metadata

Assignees

Labels

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions