jdk/src/share/classes/javax/sound/midi/MidiFileFormat.java
changeset 25131 49006bd0e69d
parent 22584 eed64ee05369
child 26003 d630c97424bd
--- a/jdk/src/share/classes/javax/sound/midi/MidiFileFormat.java	Thu Jun 05 10:37:24 2014 -0700
+++ b/jdk/src/share/classes/javax/sound/midi/MidiFileFormat.java	Thu Jun 05 23:17:05 2014 -0700
@@ -266,6 +266,7 @@
      * @see #getProperty(String)
      * @since 1.5
      */
+    @SuppressWarnings("unchecked") // Cast of result of clone
     public Map<String,Object> properties() {
         Map<String,Object> ret;
         if (properties == null) {