diff options
| author | aarne <aarne@cs.chalmers.se> | 2007-11-06 14:44:17 +0000 |
|---|---|---|
| committer | aarne <aarne@cs.chalmers.se> | 2007-11-06 14:44:17 +0000 |
| commit | 2b1d5a4d513970308f47c735212cbc253ec40961 (patch) | |
| tree | 2395299df4ba44d7cfb060b9294ea38f1dce63f4 /src/Makefile | |
| parent | 693621ffbe9146f24ba75e073b6ce2e716c56a5e (diff) | |
Devel/GF3: experimentally putting together all functionalities for the first time
Diffstat (limited to 'src/Makefile')
| -rw-r--r-- | src/Makefile | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Makefile b/src/Makefile index 690b66cee..6cda7d458 100644 --- a/src/Makefile +++ b/src/Makefile @@ -203,6 +203,11 @@ gfcc: strip gfcc mv gfcc ../bin/ +gf3: + $(GHMAKE) $(GHCOPTFLAGS) -o gf3 GF/Devel/GF3.hs + strip gf3 + mv gf3 ../bin/ + gfcc2c: $(MAKE) -C tools/c $(MAKE) -C ../lib/c |