diff options
Diffstat (limited to 'Makefile.config')
| -rw-r--r-- | Makefile.config | 47 |
1 files changed, 0 insertions, 47 deletions
diff --git a/Makefile.config b/Makefile.config deleted file mode 100644 index d070d82feb..0000000000 --- a/Makefile.config +++ /dev/null @@ -1,47 +0,0 @@ -### Compile-time configuration - -### Which C compiler to use. -### Performance is *much* better if Gnu CC 2 is used. -CC=gcc -#CC=cc - -### Additional compile-time options -# If using gcc on Intel 386 or Motorola 68k: -# CCCOMPOPTS=-fno-defer-pop -# If using gcc and being superstitious: -CCCOMPOPTS=-Wall -# Otherwise: -# CCCOMPOPTS= - -### Additional link-time options -CCLINKOPTS= - -### If using GCC on a Dec Alpha under OSF1: -LOWADDRESSES=-Xlinker -taso -# Otherwise: -# LOWADDRESSES= - -### Libraries needed -CCLIBS=$(TERMINFOLIBS) -lm - -### How to invoke ranlib (if needed) -# BSD-style: -RANLIB=ranlib -# System V-style: -# RANLIB=ar -rs -# If ranlib is not needed at all: -# RANLIB=true - -### Do #! scripts work on your system? -SHARPBANGSCRIPTS=true -# SHARPBANGSCRIPTS=false - -### Where to install the binaries -BINDIR=/usr/local/bin - -### Where to install the standard library -LIBDIR=/usr/local/lib/camlsl - -### Where to install the man pages -MANDIR=/usr/local/man/man1 -MANEXT=1 |