diff options
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 7 |
1 files changed, 1 insertions, 6 deletions
@@ -19,14 +19,9 @@ # can just use the defaults, fortunately. # You need a full complement of GNU utilities to run this Makefile -# successfully; most notably, you need bash, GNU make, flex (>= 2.5.1) +# successfully; most notably, you need GNU make, flex (>= 2.5.1) # and bison. -# If your /bin/sh is not bash, change the below definition so that make can -# find bash. Or you can hope your sh-like shell understands all scripts. -# I think so, but I have not tested it. -#SHELL := /usr/bin/bash - # Uncomment the second line if you are a developer. This will enable many # additional warnings at compile-time #WARN := 0 |