I have a question about the install rule in the main Makefile: what is the purpose of $(DESTDIR)? Why is the default to install into an install directory? -- Filip Pizlo http://bocks.psych.purdue.edu/ pizlo@purdue.edu