From f7bff16c9a36baa91847cfb2f609084a43bcc9a1 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 28 Aug 2023 14:45:45 +0200
Subject: [PATCH] fix: If src is a dir, assume the lean file has the full path
 (#2465)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

It seems that before, if `$src` isn’t a file, but a directory, that it
would contain `Bar.lean` directly, and not `Foo/Bar.lean`. This seemd
odd and would not allow dependencies to be included easily.
---
 nix/buildLeanPackage.nix | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix
index b8fa77ce89..4ae908836d 100644
--- a/nix/buildLeanPackage.nix
+++ b/nix/buildLeanPackage.nix
@@ -158,7 +158,7 @@ with builtins; let
     buildCommand = ''
       dir=$(dirname $relpath)
       mkdir -p $dir $out/$dir $ilean/$dir $c/$dir
-      if [ -d $src ]; then cp -r $src/. $dir/; else cp $src $leanPath; fi
+      if [ -d $src ]; then cp -r $src/. .; else cp $src $leanPath; fi
       lean -o $out/$oleanPath -i $ilean/$ileanPath -c $c/$cPath $leanPath $leanFlags $leanPluginFlags $leanLoadDynlibFlags
     '';
   }) // {