File tree Expand file tree Collapse file tree 3 files changed +3
-3
lines changed
Expand file tree Collapse file tree 3 files changed +3
-3
lines changed Original file line number Diff line number Diff line change @@ -449,7 +449,7 @@ the `update-alternatives` approach.)
449449
450450 ```bash
451451 nix develop
452- emacs src/Ledger.agda
452+ emacs src/Ledger.lagda.md
453453 ```
454454
4554553. Use standard `agda-mode` commands (e.g., `C-c C-l` to load a file).
Original file line number Diff line number Diff line change @@ -28,7 +28,7 @@ mkDerivation {
2828 iog-prelude
2929 ] ;
3030 buildPhase = ''
31- agda --profile=modules src/Ledger.agda | tee typecheck.log
31+ agda --profile=modules src/Ledger.lagda.md | tee typecheck.log
3232 '' ;
3333 doCheck = true ;
3434 checkPhase = ''
Original file line number Diff line number Diff line change 4949----------------------------
5050Add something like this to any generated Markdown for which the true source is known:
5151---
52- source_path: src/Ledger/Prelude.agda
52+ source_path: src/Ledger/Prelude.lagda.md
5353source_branch: master
5454---
5555
You can’t perform that action at this time.
0 commit comments