diff Makefile.in @ 502:8875ff2e85dc

Profiling support
author Adam Chlipala <adamc@hcoop.net>
date Thu, 20 Nov 2008 12:16:30 -0500
parents 24d22b843729
children ca95f9e4d45f
line wrap: on
line diff
--- a/Makefile.in	Thu Nov 20 11:34:36 2008 -0500
+++ b/Makefile.in	Thu Nov 20 12:16:30 2008 -0500
@@ -21,10 +21,10 @@
 	rm -rf .cm src/.cm
 
 clib/urweb.o: src/c/urweb.c
-	gcc -O3 -I include -c src/c/urweb.c -o clib/urweb.o
+	gcc -O3 -I include -c src/c/urweb.c -o clib/urweb.o $(CFLAGS)
 
 clib/driver.o: src/c/driver.c
-	gcc -O3 -I include -c src/c/driver.c -o clib/driver.o
+	gcc -O3 -I include -c src/c/driver.c -o clib/driver.o $(CFLAGS)
 
 src/urweb.cm: src/prefix.cm src/sources
 	cat src/prefix.cm src/sources \