godot_headers: remove in favour of godot.dev

This commit is contained in:
James Kay 2018-03-28 12:43:45 +01:00
parent 76f32d9b41
commit a811d1d6cc
No known key found for this signature in database
GPG key ID: 76BE7F17BF11AD15
2 changed files with 0 additions and 24 deletions

View file

@ -1,23 +0,0 @@
{ stdenv, fetchFromGitHub }:
stdenv.mkDerivation rec {
name = "godot_headers";
version = "2018-02-09";
src = fetchFromGitHub {
owner = "GodotNativeTools";
repo = "godot_headers";
rev = "51bca3bf5d917341f3e15076c5a9191f8a5118ae";
sha256 = "0z562pqm8y8wldmfiya72cvwwpvcfznpl0wypagw50v0f41ilywh";
};
buildPhase = "true";
installPhase = ''
mkdir $out
cp -r . $out/include
'';
meta = {
homepage = "https://github.com/GodotNativeTools/godot_headers/";
description = "Headers for the Godot API supplied by the GDNative module";
license = stdenv.lib.licenses.mit;
platforms = stdenv.lib.platforms.all;
maintainers = [ stdenv.lib.maintainers.twey ];
};
}

View file

@ -2623,7 +2623,6 @@ with pkgs;
gocryptfs = callPackage ../tools/filesystems/gocrypfs { };
godot = callPackage ../development/tools/godot {};
godot_headers = callPackage ../development/libraries/godot_headers {};
goklp = callPackage ../tools/networking/goklp {};