mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 04:33:45 +03:00
Remove stale src/IdrisPath.idr on each 'make clean' run
${PREFIX} can now be properly changed on each rebuild
This commit is contained in:
parent
1fb8904992
commit
ebb98700bf
1
Makefile
1
Makefile
@ -81,6 +81,7 @@ clean-libs:
|
||||
|
||||
clean: clean-libs support-clean
|
||||
-${IDRIS2_BOOT} --clean ${IDRIS2_IPKG}
|
||||
$(RM) src/IdrisPaths.idr
|
||||
${MAKE} -C tests clean
|
||||
$(RM) -r build
|
||||
|
||||
|
0
bootstrap.sh
Executable file → Normal file
0
bootstrap.sh
Executable file → Normal file
Loading…
Reference in New Issue
Block a user