idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-20 01:41:44 +03:00
Code Issues Projects Releases Wiki Activity
3,492 Commits 6 Branches 9 Tags 115 MiB
017608fa12
Commit Graph

70 Commits

Author SHA1 Message Date
Edwin Brady
824b661cd5 Update bootstrap scheme 
The library code uses a new feature, and it needs to be able to build
with the bootstrap code (though, fortunately, not with idris2-boot)
 2020-05-22 18:06:04 +01:00
Niklas Larsson
d50bb099ea Windows support 2020-05-21 15:13:06 +02:00
Kamil Shakirov
f696335f2d Rename some file/dir manipulation functions 
Renamed:

fileRemove -> removeFile

dirOpen -> openDir
dirClose -> closeDir
rmDir -> removeDir
 2020-05-21 18:32:35 +06:00
Edwin Brady
ac859a9c50 Move bootstrap racket to the right place 2020-05-20 16:55:20 +01:00
Edwin Brady
43ef716fa8 Update idris2-boot 2020-05-20 14:27:26 +01:00
Edwin Brady
b94ff558f3 Put idris2.ss back in the right place 2020-05-20 14:23:26 +01:00
Edwin Brady
32263883ee Update bootstrapping scripts for new exec name 
(Also, hopefully, this will poke travis to build the repo in its new
location!)
 2020-05-20 14:00:15 +01:00
Edwin Brady
746df34470 Don't overwrite idris2sh.rkt 
Better to copy and update the new version with the prefix
 2020-05-19 23:01:04 +01:00
Edwin Brady
5b88afb3ef Add racket bootstrap script 2020-05-19 22:56:27 +01:00
Edwin Brady
a5638e0aac Update bootstrap scheme 
The older version had a lingering bug from upstream Idris in writing
Integers to TTC
 2020-05-19 21:42:24 +01:00
Edwin Brady
7defc40c47 Better bootstrapping process 2020-05-19 21:08:32 +01:00
Edwin Brady
6bbb914fca
Merge pull request #1 from edwinb/remove-directory-system 
Add rmDir to System.Directory
 2020-05-19 12:24:35 +01:00
Edwin Brady
b69068f4ff Update bootstrap scripts 2020-05-18 20:33:38 +01:00
André Videla
3321dc6be3 Add rmDir to System.Directory 2020-05-18 18:28:33 +01:00
Edwin Brady
1f3c557889 Fiddle about with bootstrap scripts 
Not quite there, but nearly
 2020-05-18 18:02:56 +01:00
Edwin Brady
557de91c5a Internal errors when install fails 2020-05-18 17:15:10 +01:00
Edwin Brady
d2b652add5 Update generated scheme 2020-05-18 16:59:05 +01:00
Edwin Brady
2ef0dec192 Change boot directory 2020-05-18 16:23:37 +01:00
Edwin Brady
155dddb5f3 Another attempt at making the bootstrap step work 2020-05-18 16:02:30 +01:00
Edwin Brady
555f522ad0 Add bootstrapping instructions 
Added a known good scheme output which can be used to start the
bootstrapping process.
 2020-05-18 14:43:12 +01:00