weblint;
authorwenzelm
Tue Sep 26 17:06:16 2000 +0200 (2000-09-26)
changeset 10084ede64d0782e5
parent 10083 5c669ab41d8e
child 10085 a9704bf90031
weblint;
Admin/page/Makefile
     1.1 --- a/Admin/page/Makefile	Tue Sep 26 17:05:20 2000 +0200
     1.2 +++ b/Admin/page/Makefile	Tue Sep 26 17:06:16 2000 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4  # ---
     1.5  # --- begin rules
     1.6  
     1.7 -all: clean main dist install
     1.8 +all: clean main dist install weblint
     1.9  	@echo "###"
    1.10  	@echo "### Finished.  See main/ and dist/ for the resulting pages."
    1.11  	@echo "###"
    1.12 @@ -55,6 +55,10 @@
    1.13  install: dist
    1.14  	@cp -R dist/. ..
    1.15  
    1.16 +weblint:
    1.17 +	@weblint -x netscape $(MAIN_TARGET)
    1.18 +	@weblint -x netscape $(DIST_TARGET)
    1.19 +
    1.20  clean: 
    1.21  	@rm -rf $(MAIN_TARGET)
    1.22  	@rm -rf $(DIST_TARGET)