jmc

1
# These are the default values for plugin-specific preferences.
2
# Keys are qualified by plug-in id:
3
# 	com.example.myplugin/myproperty=myvalue
4
# "%key" are externalized strings defined in plugin_customization.properties
5
# This file does not need to be translated.
6

7
# Show progress bar in splash screen on startup.
8
org.eclipse.ui/SHOW_PROGRESS_ON_STARTUP=true
9

10
# New-style tabs by default
11
org.eclipse.ui/SHOW_TRADITIONAL_STYLE_TABS=false
12

13
# Put the perspective switcher on the top right, if one is present.
14
org.eclipse.ui/DOCK_PERSPECTIVE_BAR=topRight
15

16
# Use default accelerators
17
org.eclipse.ui/KEY_CONFIGURATION_ID=org.eclipse.ui.defaultAcceleratorConfiguration
18

19
# Set colors for the help framework interface and left toc area
20
org.eclipse.help.base/advanced.toolbarBackground=#e9e9e9
21
org.eclipse.help.base/advanced.viewBackground=#ffffff
22

23
# Set banner for help.
24
org.eclipse.help.base/banner=/org.openjdk.jmc.docs/html/banner.html
25

26
# Set height of help banner frame
27
org.eclipse.help.base/banner_height=36