]> git.tue.mpg.de Git - dss.git/commitdiff
Support local make files.
authorAndre Noll <maan@tuebingen.mpg.de>
Thu, 25 Apr 2024 13:38:23 +0000 (15:38 +0200)
committerAndre Noll <maan@tuebingen.mpg.de>
Thu, 25 Apr 2024 13:38:23 +0000 (15:38 +0200)
These additional targets are handy for site-local targets such as
installing the web files or deploying the executable and the man page
on a remote server.

.gitignore
Makefile

index 4aafb488c3fc2f1196e67b58c20b7998684a5126..36dfcfa431746cdf6c84f70d1de7e99006f3498a 100644 (file)
@@ -1,4 +1,5 @@
 Makefile.deps
+Makefile.local
 *.o
 *.swp
 dss.lsg.*
index a60a65b3e34e99f643ff4493cfff0c1b8d76a44d..c8242b4f9e3ecc96e3c7da222bf1079a05640d62 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -71,3 +71,5 @@ index.html: dss.1.html index.html.in INSTALL README NEWS
        sed -e '1,/@INSTALL@/d' -e '/@MAN_PAGE@/,$$d' index.html.in >> $@
        cat dss.1.html >> $@
        sed -e '1,/@MAN_PAGE@/d' index.html.in >> $@
+
+-include Makefile.local