Merge pull request #2996 from FStarLang/_nik_ide_id_info #2461

Triggered via push July 26, 2023 05:22

nikswamy

master

Status Success

Total duration 9m 40s

Artifacts 2

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	116 KB
Resource usage information (summary) Expired	3.96 KB