Open LeifW opened 10 years ago
Basically, the fun I had here: https://github.com/idris-lang/Idris-dev/issues/954 If the change described on #6 is made, I can get a proper definition from \d, and \c, but can't \t or \o. Removing syntastic 3.3.0_113_g0de089b entirely seems to fix everything. This became a bigger issue after https://github.com/idris-lang/Idris-dev/commit/2df0a7f7ae6063ce50d52271631d75db6c2d4775, as .ibcs weren't being saved for files w/ metavars before that. syntastic may not be that useful given #1 - \r can be used instead.
Basically, the fun I had here: https://github.com/idris-lang/Idris-dev/issues/954 If the change described on #6 is made, I can get a proper definition from \d, and \c, but can't \t or \o. Removing syntastic 3.3.0_113_g0de089b entirely seems to fix everything. This became a bigger issue after https://github.com/idris-lang/Idris-dev/commit/2df0a7f7ae6063ce50d52271631d75db6c2d4775, as .ibcs weren't being saved for files w/ metavars before that. syntastic may not be that useful given #1 - \r can be used instead.