fix: If src is a dir, assume the lean file has the full path (leanprover#2465)

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.

Author: nomeata

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
     '';
   }) // {