summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndre Noll <maan@tuebingen.mpg.de>2024-04-28 01:26:57 +0200
committerAndre Noll <maan@tuebingen.mpg.de>2024-04-28 01:26:57 +0200
commitffc8c4a28f52cfb0e617ec3c6f3958cd994e13b6 (patch)
tree354c4a24bc220c0fa35d1db1ea2d68d20e18aa29
parent1b576a8fa111f2001350a18635583f020c3f07c4 (diff)
parent73e0fd24ed41db7882948ee4d7ff63119cf5a67d (diff)
Merge branch 'master' into nextnext
* master: Support local make files.
-rw-r--r--.gitignore1
-rw-r--r--Makefile2
2 files changed, 3 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index 4aafb48..36dfcfa 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,5 @@
Makefile.deps
+Makefile.local
*.o
*.swp
dss.lsg.*
diff --git a/Makefile b/Makefile
index a60a65b..c8242b4 100644
--- 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