[meta] remove MicroProfile (#185)
Signed-off-by: crueter <crueter@eden-emu.dev> Reviewed-on: #185 Reviewed-by: Lizzie <lizzie@eden-emu.dev>
This commit is contained in:
parent
dbbe5b3328
commit
f1e74f6855
76 changed files with 5547 additions and 11468 deletions
|
@ -14,6 +14,8 @@ FILES=`git diff-tree --no-commit-id --name-only ${RANGE} -r`
|
|||
echo "Done"
|
||||
|
||||
for file in $FILES; do
|
||||
[ -f "$file" ] || continue
|
||||
|
||||
EXTENSION="${file##*.}"
|
||||
case "$EXTENSION" in
|
||||
kts|kt|cpp|h)
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue