mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-20 01:37:35 +03:00
Version increment
This commit is contained in:
parent
10b8698843
commit
0d81e3b59c
2
Makefile
2
Makefile
@ -10,7 +10,7 @@ TARGET = ${TARGETDIR}/${NAME}
|
||||
|
||||
MAJOR=0
|
||||
MINOR=2
|
||||
PATCH=0
|
||||
PATCH=1
|
||||
|
||||
|
||||
GIT_SHA1=
|
||||
|
@ -1,7 +1,7 @@
|
||||
$ idris hello.idr
|
||||
____ __ _ ___
|
||||
/ _/___/ /____(_)____ |__ \
|
||||
/ // __ / ___/ / ___/ __/ / Version 0.2.0
|
||||
/ // __ / ___/ / ___/ __/ / Version 0.2.1
|
||||
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
|
||||
/___/\__,_/_/ /_/____/ /____/ Type :? for help
|
||||
|
||||
|
@ -1,7 +1,7 @@
|
||||
$ idris2 interp.idr
|
||||
____ __ _ ___
|
||||
/ _/___/ /____(_)____ |__ \
|
||||
/ // __ / ___/ / ___/ __/ / Version 0.2.0
|
||||
/ // __ / ___/ / ___/ __/ / Version 0.2.1
|
||||
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
|
||||
/___/\__,_/_/ /_/____/ /____/ Type :? for help
|
||||
|
||||
|
@ -1,7 +1,7 @@
|
||||
$ idris2
|
||||
____ __ _ ___
|
||||
/ _/___/ /____(_)____ |__ \
|
||||
/ // __ / ___/ / ___/ __/ / Version 0.2.0
|
||||
/ // __ / ___/ / ___/ __/ / Version 0.2.1
|
||||
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
|
||||
/___/\__,_/_/ /_/____/ /____/ Type :? for help
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user