From 6efe13c8a1f0c03f574fce6374247ec1e560b878 Mon Sep 17 00:00:00 2001
From: "David A. Mellis" <d.mellis@arduino.cc>
Date: Sun, 16 May 2010 04:43:03 +0000
Subject: [PATCH] Fixing issue with tab menu and tabs with the same base name
 but different extensions (issue 191).

---
 app/src/processing/app/EditorHeader.java | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/app/src/processing/app/EditorHeader.java b/app/src/processing/app/EditorHeader.java
index 1dc7d4422..d40eddacf 100644
--- a/app/src/processing/app/EditorHeader.java
+++ b/app/src/processing/app/EditorHeader.java
@@ -359,7 +359,9 @@ public class EditorHeader extends JComponent {
           }
         };
       for (SketchCode code : sketch.getCode()) {
-        item = new JMenuItem(code.getPrettyName());
+        item = new JMenuItem(code.isExtension(sketch.getDefaultExtension()) ? 
+                             code.getPrettyName() : code.getFileName());
+        item.setActionCommand(code.getFileName());
         item.addActionListener(jumpListener);
         menu.add(item);
       }