From 5a126f552ec2931bdedfc4ae11f0da281c354b03 Mon Sep 17 00:00:00 2001 From: Gustavo Massaccesi Date: Thu, 29 Jan 2015 19:24:29 -0300 Subject: [PATCH] Change color in editor: Grey -> Gray --- gui-lib/mred/private/editor.rkt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gui-lib/mred/private/editor.rkt b/gui-lib/mred/private/editor.rkt index 05296fa0..4808427c 100644 --- a/gui-lib/mred/private/editor.rkt +++ b/gui-lib/mred/private/editor.rkt @@ -756,7 +756,7 @@ '("Top" "Center" "Bottom") '(top center bottom)) - (let ([colors '("Black" "White" "Red" "Orange" "Yellow" "Green" "Blue" "Purple" "Cyan" "Magenta" "Grey")]) + (let ([colors '("Black" "White" "Red" "Orange" "Yellow" "Green" "Blue" "Purple" "Cyan" "Magenta" "Gray")]) ; Colors (for-each (lambda (c)