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

leanpkg new returns failed to start child process #1975

Open
@fstiffo

Description

@fstiffo

Prerequisites

  • [X ] Put an X between the brackets on this line if you have done all of the following:
    • Checked that your issue isn't already filed.
    • Reduced the issue to a self-contained, reproducible test case.

Description

The 'leanpkg new' command does not work.

Steps to Reproduce

  1. Installed binary version of Lean on Windows
  2. Add the bin dir to PATH env var.
  3. Tested some coding on VC with the Lean extension installed, and every thing works as intended
  4. Open a cmd windows and type the command leanpkg new myfirstprj

Expected behavior: The creation of a new dir with the name myfirstprj and the setup of the project

Actual behavior: The command start and after a sec the failed to start child process error appears.

Reproduces how often: 100%

Versions

Lean (version 3.4.1, commit 17fe3de, Release)

Microsoft Windows [Version 6.1.7601]

git version 2.19.0.windows.1

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions