Skip to content

Ensure Idris is running and current idr file loaded when using idris-switch-to-repl #322

Ensure Idris is running and current idr file loaded when using idris-switch-to-repl

Ensure Idris is running and current idr file loaded when using idris-switch-to-repl #322

Triggered via pull request November 28, 2025 23:51
Status Success
Total duration 2m 3s
Artifacts

idris1.yml

on: pull_request
Matrix: build
Fit to window
Zoom out
Zoom in