Fix a stupid bug in the extension generator

diff --git a/scripts/extgen.py b/scripts/extgen.py
index ff40ec60eadd1f515336f78d4d82eec2e0cfdfff..35f016600487de594fa511d3506f77cb7e5c006b 100755 (executable)
--- a/scripts/extgen.py
+++ b/scripts/extgen.py
@@ -642,7 +642,7 @@ namespace GL {
                                supp = f.api_support.get(self.host_api.name)
                                src = None
                                for e in self.source_exts:
-                                       if f in e.things:
+                                       if f.name in e.things:
                                                src = f
                                        elif supp:
                                                for s in supp.sources: