Merge pull request #2999 from FStarLang/guido_misc #2482

Triggered via push August 1, 2023 20:52

nikswamy

master

Status Success

Total duration 8m 24s

Artifacts 2

This run and associated checks have been archived and are scheduled for deletion. Learn more about checks retention

linux-x64.yaml

on: push

2 errors

Unable to process file command 'env' successfully.

Invalid format '<html><head>'

Produced during runtime

Name	Size
Resource usage information (individual) Expired	115 KB
Resource usage information (summary) Expired	3.96 KB