From e60569995174ab119dfc7ae2bace76328bb35241 Mon Sep 17 00:00:00 2001 From: "Kartik K. Agaram" Date: Wed, 9 Mar 2016 03:31:56 -0800 Subject: 2744 Tweak colors and font-sizes in generated html. --- html/edit/001-editor.mu.html | 4 ++-- html/edit/002-typing.mu.html | 4 ++-- html/edit/003-shortcuts.mu.html | 4 ++-- html/edit/004-programming-environment.mu.html | 4 ++-- html/edit/005-sandbox.mu.html | 4 ++-- html/edit/006-sandbox-edit.mu.html | 4 ++-- html/edit/007-sandbox-delete.mu.html | 4 ++-- html/edit/008-sandbox-test.mu.html | 4 ++-- html/edit/009-sandbox-trace.mu.html | 4 ++-- html/edit/010-errors.mu.html | 4 ++-- html/edit/011-editor-undo.mu.html | 4 ++-- 11 files changed, 22 insertions(+), 22 deletions(-) (limited to 'html/edit') diff --git a/html/edit/001-editor.mu.html b/html/edit/001-editor.mu.html index 4ca8b427..54f91eb8 100644 --- a/html/edit/001-editor.mu.html +++ b/html/edit/001-editor.mu.html @@ -10,8 +10,8 @@