Admin/website/makefile
author wenzelm
Wed, 21 Sep 2005 21:01:27 +0200
changeset 17576 3be0d6cfbc3a
parent 16233 e634d33deb86
permissions -rw-r--r--
echo HOL_USEDIR_OPTIONS;

# isaweb makefile
# $Id$

# just delegate
include build/main.mak