From c5d078e01fc0f707f43b6aedcd863bf5b67b50e2 Mon Sep 17 00:00:00 2001
From: Kevin Arlin <arlinkevind@gmail.com>
Date: Mon, 29 Apr 2024 15:08:53 -0700
Subject: [PATCH] add comment

---
 src/plfa/part1/Naturals.lagda.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/plfa/part1/Naturals.lagda.md b/src/plfa/part1/Naturals.lagda.md
index 102477a0c..71d26f6ff 100644
--- a/src/plfa/part1/Naturals.lagda.md
+++ b/src/plfa/part1/Naturals.lagda.md
@@ -838,6 +838,9 @@ filled, you can type `C-c C-space`, which will remove the hole:
     zero + n = n
     suc m + n = { }1
 
+Note: `C-space` may be a reserved command on Mac OS X, in which case
+try typing `C-c C-r` instead.
+
 Again, going into hole 1 and typing `C-c C-,` will display information on the
 required type of the hole, and what free variables are available: