tweaks to playground files

This commit is contained in:
2024-11-25 16:25:05 -08:00
parent acb37a2882
commit 6f954b1183
4 changed files with 36 additions and 67 deletions

View File

@@ -1,6 +1,8 @@
## TODO
- [ ] add filenames to FC
- [ ] add namespaces
- [ ] imported files leak info messages everywhere
- For now, take the start ix for the file and report at end starting there
- [ ] update node shim to include idris2-playground changes