From 1775aa192666f278a44031ac967aea6aad3e2706 Mon Sep 17 00:00:00 2001
From: Paul Eggert <eggert@cs.ucla.edu>
Date: Wed, 18 Jul 2018 04:33:52 -0700
Subject: [PROPOSED] * Makefile: Add mawk comment.

---
 Makefile | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Makefile b/Makefile
index b8a1a62..94b6423 100644
--- a/Makefile
+++ b/Makefile
@@ -367,6 +367,9 @@ ZFLAGS=
 ZIC_INSTALL=	$(ZIC) -d '$(DESTDIR)$(TZDIR)' $(LEAPSECONDS)
 
 # The name of a Posix-compliant 'awk' on your system.
+# Older 'mawk' versions, such as the 'mawk' in Ubuntu 16.04, might dump core;
+# on Ubuntu you can work around this with
+#	AWK=		gawk
 AWK=		awk
 
 # The full path name of a Posix-compliant shell, preferably one that supports
-- 
2.7.4