[Agda-dev] update to Agda.cabal

[Andreas Abel]

This warning has been fixed by

commit 7b312d9f90055850ca07618122d406889d4d5bb0
Author: Robert Estelle <robertestelle at gmail.com>
Date:   Thu Aug 13 18:34:39 2020 -0700

     hlint: Fix trivial functor law suggestion

     The warning was:
     Functor law:
     Found: "render <$> pretty\n <$> runAbsToCon (lookupQName 
AmbiguousNothing $ I.conName v)"
     Perhaps: "render . pretty\n <$> runAbsToCon (lookupQName 
AmbiguousNothing $ I.conName v)"


On 2020-08-13 22:53, John Leo wrote:
> Actually I'm getting some kind of hlint warning but it looks like it's 
> from someone else's change.
> https://github.com/agda/agda/runs/982268192
> 
> John
> 
> On Thu, Aug 13, 2020 at 1:51 PM John Leo <leo at halfaya.org 
> <mailto:leo at halfaya.org>> wrote:
> 
>     Hi everyone,
> 
>     I updated GHC to 8.10.2 today, downloaded the latest Agda master,
>     and compiled. I was able to typecheck and also compile MusicTools
>     and everything worked fine.
> 
>     The only change I had to make was to loosen a bound in Agda.cabal.
>     Rather than create a new branch, modify the file there and submit a
>     pull request I just pushed to Master. I hope that is okay since it's
>     a trivial and safe change, but feel free to revert if you feel there
>     might be some problem.
> 
>     John
> 
> 
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
> 

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/