I want to change the editor’s font and enable ligatures. The problem is I don’t know which fonts are avaliable in the online editor, and which of them support ligatures. The workbench.colorTheme option for example has an edit button next to it which shows me which themes are avaliable in the online editor. However, the editor.fontFamily option has no such button, and I can’t know which fonts I can use. I couldn’t find a list of avaliable fonts online. Is such a list avaliable somewhere?
Perhaps, the edit button should also be integrated with the editor.fontFamily option.
I guess you can use any font installed on your system and recognised by your browser.