Index: src/org/openstreetmap/josm/gui/MapMover.java
===================================================================
--- src/org/openstreetmap/josm/gui/MapMover.java	(revision 381)
+++ src/org/openstreetmap/josm/gui/MapMover.java	(working copy)
@@ -92,7 +92,7 @@
 	/**
 	 * If the right (and only the right) mouse button is pressed, move the map
 	 */
-	public void mouseDragged(MouseEvent e) {
+	@Override public void mouseDragged(MouseEvent e) {
 		int offMask = MouseEvent.BUTTON1_DOWN_MASK | MouseEvent.BUTTON2_DOWN_MASK;
 		if ((e.getModifiersEx() & (MouseEvent.BUTTON3_DOWN_MASK | offMask)) == MouseEvent.BUTTON3_DOWN_MASK) {
 			if (mousePosMove == null)
@@ -157,7 +157,7 @@
 	 * Zoom the map by 1/5th of current zoom per wheel-delta.
 	 * @param e The wheel event.
 	 */
-	public void mouseWheelMoved(MouseWheelEvent e) {
+	@Override public void mouseWheelMoved(MouseWheelEvent e) {
 		int w = nc.getWidth();
 		int h = nc.getHeight();
 
@@ -176,5 +176,5 @@
 	/**
 	 * Does nothing. Only to satisfy MouseMotionListener
 	 */
-	public void mouseMoved(MouseEvent e) {}
+	@Override public void mouseMoved(MouseEvent e) {}
 }
