From 89e87380d85f8126c5c3ef4e3ccecbc2e7852fc3 Mon Sep 17 00:00:00 2001 From: Ariel Abreu Date: Wed, 29 Jul 2020 10:37:31 -0400 Subject: [PATCH] Update man [skip ci] I'm going to start skipping the CI for these simple update commits; I'll do a CI commit later after updating a bunch of the little submodules (this way, we save on our allotted build minutes on CircleCI) --- src/external/man | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/external/man b/src/external/man index 519d0b90b..aed05506a 160000 --- a/src/external/man +++ b/src/external/man @@ -1 +1 @@ -Subproject commit 519d0b90b2880ad737fda418afb07a4e0d683ecd +Subproject commit aed05506a296bffe47e5dfa9e461cdd4f37e1542