Skip to content
This repository has been archived by the owner on Oct 14, 2023. It is now read-only.

fix(library/init):removed unused import #1983

Closed
wants to merge 1 commit into from
Closed

fix(library/init):removed unused import #1983

wants to merge 1 commit into from

Commits on Nov 29, 2018

  1. fix(library/init):remove unused import 

    the low level export of the library is not working with the import of the init.version, that was added to .gitignore since release 3.4.0
Closes leanprover#1964
    @harry239
    harry239 committed Nov 29, 2018
    Configuration menu
    Copy the full SHA
    75602ec View commit details
    Browse the repository at this point in the history