From dc307b985228a1c073aaecd74d2fd7e8447d709d Mon Sep 17 00:00:00 2001
From: "U-Huygens-PC\\Bibibi" <eziopsx@gmail.com>
Date: Tue, 9 Aug 2016 19:47:29 +0200
Subject: [PATCH] Remove unused stuff

---
 dist-scripts/dist-cores.sh | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/dist-scripts/dist-cores.sh b/dist-scripts/dist-cores.sh
index 51c2c1d820..b437f36e26 100755
--- a/dist-scripts/dist-cores.sh
+++ b/dist-scripts/dist-cores.sh
@@ -165,9 +165,7 @@ for f in `ls -v *_${platform}.${EXT}`; do
    fi
 
    # Compile core
-   if [ $PLATFORM = "ode-ps3" ] ; then
-      make -C ../ -f Makefile.${platform}.cobra $whole_archive -j3 || exit 1
-   elif [ $MAKEFILE_GRIFFIN = "yes" ]; then
+   if [ $MAKEFILE_GRIFFIN = "yes" ]; then
       make -C ../ -f Makefile.griffin platform=${platform} $whole_archive $big_stack -j3 || exit 1
    elif [ $PLATFORM = "emscripten" ]; then
       make -C ../ -f Makefile.emscripten LTO=$lto -j7 || exit 1