diff Makefile.in @ 430:0af37c883358

mkdir -p BIN
author Adam Chlipala <adamc@hcoop.net>
date Sat, 25 Oct 2008 12:18:33 -0400
parents 0eb7bb4872d0
children 24d22b843729
line wrap: on
line diff
--- a/Makefile.in	Sat Oct 25 12:07:10 2008 -0400
+++ b/Makefile.in	Sat Oct 25 12:18:33 2008 -0400
@@ -59,6 +59,7 @@
 	$(MLTON) -output $@ src/urweb.mlb
 
 install:
+	mkdir -p $(BIN)
 	cp bin/urweb $(BIN)/
 	mkdir -p $(LIB_UR)
 	cp lib/*.urs $(LIB_UR)/