idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 09:12:34 +03:00
Code Issues Projects Releases Wiki Activity
86c060ef13
Idris2/tests/node/nomangle002
History
Zoe Stafford 86c060ef13
Reimplement %nomangle in terms of %export (#2604) 
* Reimplement %nomangle in terms of %export
Also deprecate %nomangle

* [ lint ] fix linter errors
2022-08-15 13:26:06 +01:00
..
expected Reimplement %nomangle in terms of %export (#2604) 2022-08-15 13:26:06 +01:00
nomangle1.idr Reimplement %nomangle in terms of %export (#2604) 2022-08-15 13:26:06 +01:00
nomangle2.idr Reimplement %nomangle in terms of %export (#2604) 2022-08-15 13:26:06 +01:00
run [ new ] Add %nomangle (#2063) 2021-11-09 16:23:50 +00:00