Skip to content

Commit

Permalink
[ #3159 ] Added missing replace.
Browse files Browse the repository at this point in the history
Replaced `--no-default-libraries` by `--no-libraries`.

(cherry picked from commit 8f0c5d7)
  • Loading branch information
asr committed Jul 18, 2018
1 parent f6019b5 commit 1aa797d
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion examples/Makefile
Expand Up @@ -26,7 +26,7 @@ default : ac \

agda = $(AGDA_BIN)

run_agda = $(agda) -v0 --vim --ignore-interfaces --no-default-libraries
run_agda = $(agda) -v0 --vim --ignore-interfaces --no-libraries

other_files = AIM5/Hedberg/SET.agda \
AIM5/yoshiki/SET.agda \
Expand Down

0 comments on commit 1aa797d

Please sign in to comment.