Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Use YYYY-MM-DDTHH_MM_SS as datetime format for ICE dump files #116814

Merged
merged 1 commit into from
Oct 18, 2023
Merged

Use YYYY-MM-DDTHH_MM_SS as datetime format for ICE dump files #116814

merged 1 commit into from
Oct 18, 2023

Commits on Oct 17, 2023

  1. Use YYYY-MM-DDTHH_MM_SS as datetime format for ICE dump files 

    Windows paths do not support `:`, so use a datetime format in ICE dump
paths that Windows will accept.

Fix rust-lang#116809, fix rust-lang#115180.
    @estebank
    estebank committed Oct 17, 2023
    Configuration menu
    Copy the full SHA
    e1aa5ad View commit details
    Browse the repository at this point in the history