d7d28c fix the noextensions option (#830266)

Authored and Committed by ovasik 7 years ago
    fix the noextensions option (#830266)
    
        
file modified
+6 -1