Skip to content
This repository has been archived by the owner on Jul 25, 2022. It is now read-only.

Try to launch ENSIME server #3

Merged
merged 5 commits into from
Nov 24, 2017
Merged

Try to launch ENSIME server #3

merged 5 commits into from
Nov 24, 2017

Commits on Nov 20, 2017

  1. Added plugin configuration schema

    @laughedelic
    laughedelic committed Nov 20, 2017
    Configuration menu
    Copy the full SHA
    6a72b0a View commit details
    Browse the repository at this point in the history

  2. Added package.json to gitignore

    @laughedelic
    laughedelic committed Nov 20, 2017
    Configuration menu
    Copy the full SHA
    0eca3c9 View commit details
    Browse the repository at this point in the history

  3. Added server type

    @laughedelic
    laughedelic committed Nov 20, 2017
    Configuration menu
    Copy the full SHA
    d90f559 View commit details
    Browse the repository at this point in the history

  4. Using different server depending on the settings

    @laughedelic
    laughedelic committed Nov 20, 2017
    Configuration menu
    Copy the full SHA
    01d2dcf View commit details
    Browse the repository at this point in the history

Commits on Nov 21, 2017

  1. Changed to the official (but still experimental) ENSIME LSP server

    @laughedelic
    laughedelic committed Nov 21, 2017
    Configuration menu
    Copy the full SHA
    473f62c View commit details
    Browse the repository at this point in the history