diff options
| author |  Benjamin Barenblat <bbarenblat@galois.com> | 2014-01-24 17:08:55 -0800 |
|---|---|---|
| committer | Benjamin Barenblat <bbarenblat@galois.com> | 2014-01-24 17:08:55 -0800 |
| commit | f767413fbe1cc74d66233c9ff5df3895a528b5d5 (patch) | |
| tree | 071c9ef4d697c11b6a5b87b393f699fa75c7b7b0 | |
| parent | 02b884ea4eab34b0114043dbf24c2ee8e4a66ca7 (diff) | |
The software’s name is officially spelled “Firefox,” without
camel-casing. It’s already spelled that way throughout most of the
package, but there were a couple places where camel-casing persisted.
| -rw-r--r-- | README.md | 2 | ||||
| -rw-r--r-- | doc/manual_src/gettingStarted.md | 4 | ||||
| -rw-r--r-- | src/batchtools/webdrivers/src/main/java/com/galois/fiveui/drivers/Drivers.java | 2 |
3 files changed, 4 insertions, 4 deletions
@@ -10,7 +10,7 @@ Google Chrome. If you're familiar with browser extensions, you can quickly install FiveUI from the binaries: - Chrome: [fiveui.crx](http://galoisinc.github.com/FiveUI/binaries/fiveui.crx) - - FireFox: [fiveui.xpi](http://galoisinc.github.com/FiveUI/binaries/fiveui.xpi) + - Firefox: [fiveui.xpi](http://galoisinc.github.com/FiveUI/binaries/fiveui.xpi) The [Installation Guide](doc/manual_src/install.md) describes the installation process for Firefox and Google Chrome. diff --git a/doc/manual_src/gettingStarted.md b/doc/manual_src/gettingStarted.md index 9928916..4167584 100644 --- a/doc/manual_src/gettingStarted.md +++ b/doc/manual_src/gettingStarted.md @@ -22,9 +22,9 @@ options link on the extensions page, or through the options item on the context menu off of the FiveUI button (accessed by right-clicking on the FiveUI button). -## Options in FireFox +## Options in Firefox -The options page in `FireFox` can be accessed via the FiveUI gear widget, which +The options page in `Firefox` can be accessed via the FiveUI gear widget, which should be added in addition to the FiveUI widget when the addon is installed. Once clicked, a new tab should appear which serves as the options interface for the addon. diff --git a/src/batchtools/webdrivers/src/main/java/com/galois/fiveui/drivers/Drivers.java b/src/batchtools/webdrivers/src/main/java/com/galois/fiveui/drivers/Drivers.java index 7e53d06..6450e25 100644 --- a/src/batchtools/webdrivers/src/main/java/com/galois/fiveui/drivers/Drivers.java +++ b/src/batchtools/webdrivers/src/main/java/com/galois/fiveui/drivers/Drivers.java @@ -80,7 +80,7 @@ public class Drivers { FirefoxDriver driver; if (null == ffBinaryPath) { System.err - .println("WARNING: Running essentially random version of FireFox!"); + .println("WARNING: Running essentially random version of Firefox!"); System.err.println(" set a path to firefox with -D" + FIREFOX_BIN_PATH + "=<path to firefox>"); driver = new FirefoxDriver(profile); |