Rename gerrit module to gerrit_ui

This frees up the name 'gerrit' in the top level page, making it
available for us to start publishing a JavaScript native API for
plugins to connect with the UI.

Change-Id: I71f374d7231859dc1ed7d8a0df27759dbfc1315f
This commit is contained in:
Shawn O. Pearce
2012-10-11 22:24:04 -07:00
parent 073da8a50a
commit 1915b91937
6 changed files with 8 additions and 8 deletions

View File

@@ -13,7 +13,7 @@
See the License for the specific language governing permissions and
limitations under the License.
-->
<module rename-to="gerrit">
<module rename-to="gerrit_ui">
<inherits name='com.google.gwt.editor.Editor'/>
<inherits name='com.google.gwt.user.User'/>
<inherits name='com.google.gwt.resources.Resources'/>

View File

@@ -13,7 +13,7 @@
See the License for the specific language governing permissions and
limitations under the License.
-->
<module rename-to="gerrit">
<module rename-to="gerrit_ui">
<inherits name='com.google.gerrit.GerritGwtUI'/>
<set-property name="user.agent" value="gecko1_8" />
<set-property name="locale" value="default" />

View File

@@ -13,7 +13,7 @@
See the License for the specific language governing permissions and
limitations under the License.
-->
<module rename-to="gerrit">
<module rename-to="gerrit_ui">
<inherits name='com.google.gerrit.GerritGwtUI'/>
<set-property name="user.agent" value="safari" />
<set-property name="locale" value="default" />