From 744e799bdaad748a6069a1f3fe8a25c708317c25 Mon Sep 17 00:00:00 2001
From: Seth Greenstein <sgreenstein@users.noreply.github.com>
Date: Mon, 15 Jul 2019 16:40:57 -0700
Subject: [PATCH] Change "python" to "python_headers" in comment (#6046)

Following the instructions as is does not work, the new_local_repository rule needs to be called "python_headers"
---
 util/python/BUILD | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/util/python/BUILD b/util/python/BUILD
index 3ac0385669..ef2238a83b 100644
--- a/util/python/BUILD
+++ b/util/python/BUILD
@@ -9,7 +9,7 @@
 # includes the following local_repository rule that points to this directory:
 #
 # new_local_repository(
-#   name = "python",
+#   name = "python_headers",
 #   path = __workspace_dir__ + "/util/python",
 # )
 cc_library(