idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-13 05:48:39 +03:00
Code Issues Projects Releases Wiki Activity

Mark IdrisPaths.idr @generated

Browse Source
This commit is contained in:
Stiopa Koltsov 2021-01-16 08:28:56 +00:00 committed by G. Allais
parent 1376bdf3f2
commit 0e0b45e666
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Makefile
View File

@ -59,7 +59,8 @@ ${TARGET}: src/IdrisPaths.idr
# We use FORCE to always rebuild IdrisPath so that the git SHA1 info is always up to date
src/IdrisPaths.idr: FORCE
echo 'module IdrisPaths' > src/IdrisPaths.idr
echo '-- @generated' > src/IdrisPaths.idr
echo 'module IdrisPaths' >> src/IdrisPaths.idr
echo 'export idrisVersion : ((Nat,Nat,Nat), String); idrisVersion = ((${MAJOR},${MINOR},${PATCH}), "${GIT_SHA1}")' >> src/IdrisPaths.idr
echo 'export yprefix : String; yprefix="${IDRIS2_PREFIX}"' >> src/IdrisPaths.idr