Important changes to forums and questions

All forums and questions are now archived. To start a new conversation or read the latest updates go to forums.mbed.com.

Tip: changing source code editor font in the online IDE for Safari

Topic last updated 16 Feb 2015, by Prashant Vaibhav. 0 replies
Prashant Vaibhav
16 Feb 2015

Hi all,

Thought I'll share a tip for changing the text editor font (finally!) if you're using Safari. (There are extensions for Chrome apparently, but nothing so far for Safari).

1. Download and install the extension from here: http://code.grid.in.th

2. Then click the "A" icon it puts on your Safari toolbar, and make a new rule with the following properties:

Name: mbed font (or whatever you want)

Includes: https://developer.mbed.org/compiler/*

Styles:

.EDITOR_CURSOR, .EDITOR_LINE, .EDITOR_LINE_TEST, .EDITOR_NUMBER, .EDITOR_SELECT, .EDITOR_INPUT {
font-family: "Consolas" !important;
}

Then hit Save and you're done! The actual font can be changed in line 2 of the CSS above. Enjoy!