/ide should always use default theme

Signed-off-by: Christopher Guindon <chris.guindon@eclipse-foundation.org>
3 files changed
tree: dc0356a81a796e006854e13a4d265ba217bf7477
  1. content/
  2. images/
  3. index.php