From 60ea0f0cd5d1db3f537a9e56cfb05281ff96eb95 Mon Sep 17 00:00:00 2001
From: Peli de Halleux <pelikhan@users.noreply.github.com>
Date: Wed, 19 Sep 2018 11:27:30 -0700
Subject: [PATCH] allow for numbers in filename filter

---
 pxtarget.json | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pxtarget.json b/pxtarget.json
index 9e82b8d5..58410ec9 100644
--- a/pxtarget.json
+++ b/pxtarget.json
@@ -177,7 +177,7 @@
         "monacoColors": {
             "editor.background": "#f9f9f9"
         },
-        "fileNameExclusiveFilter": "[^a-zA-Z]"
+        "fileNameExclusiveFilter": "[^a-zA-Z0-9]"
     },
     "ignoreDocsErrors": true
 }