diff options
| author | peb <unknown> | 2005-03-07 11:44:09 +0000 |
|---|---|---|
| committer | peb <unknown> | 2005-03-07 11:44:09 +0000 |
| commit | dcf87cd664f0787be5144c0dfb0d480e6ee26946 (patch) | |
| tree | debcae6b20441264e8548c2fc5378fdeaa41762e | |
| parent | b2fa8408c6023b052c2c5df600e93b6aa3772968 (diff) | |
"Committed_by_peb"
| -rw-r--r-- | src/Makefile | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Makefile b/src/Makefile index 396abecea..5799f86ca 100644 --- a/src/Makefile +++ b/src/Makefile @@ -115,6 +115,9 @@ tracing: strip gf mv gf ../bin/ +ghci-trace: nofud-links + $(GHCI) $(GHCFLAGS) -itrace $(GHCINCLUDENOFUD) + prof: GHCOPTFLAGS += -prof -auto-all -auto-dicts prof: all |