Bug#955494: `menhir --suggest-menhirLib` suggests wrong directory

To: Stéphane Glondu <glondu@debian.org>, 955494@bugs.debian.org
Subject: Bug#955494: `menhir --suggest-menhirLib` suggests wrong directory
From: Ralf Treinen <treinen@free.fr>
Date: Thu, 2 Apr 2020 09:04:23 +0200
Message-id: <[🔎] 20200402070423.GH939387@seneca.home.org>
Reply-to: Ralf Treinen <treinen@free.fr>, 955494@bugs.debian.org
In-reply-to: <[🔎] 158575456481.3372375.11006269696689008982.reportbug@malt.loria.fr>
References: <[🔎] 158575456481.3372375.11006269696689008982.reportbug@malt.loria.fr> <[🔎] 158575456481.3372375.11006269696689008982.reportbug@malt.loria.fr>

Hello Stéphane,

On Wed, Apr 01, 2020 at 05:22:44PM +0200, Stéphane Glondu wrote:
> Severity: important

> `menhir --suggest-menhirLib` returns `/usr/lib/menhirLib` which does
> not exist. It think it should return `/usr/lib/ocaml/menhirLib`.

why severity=important ? I wasn't even aware of this option.

-Ralf.

Reply to:

Follow-Ups:
- Bug#955494: `menhir --suggest-menhirLib` suggests wrong directory
  - From: Stéphane Glondu <glondu@debian.org>

References:
- Bug#955494: `menhir --suggest-menhirLib` suggests wrong directory
  - From: Stéphane Glondu <glondu@debian.org>

Prev by Date: Bug#955494: `menhir --suggest-menhirLib` suggests wrong directory
Next by Date: Bug#955494: `menhir --suggest-menhirLib` suggests wrong directory
Previous by thread: Bug#955494: `menhir --suggest-menhirLib` suggests wrong directory
Next by thread: Bug#955494: `menhir --suggest-menhirLib` suggests wrong directory
Index(es):
- Date
- Thread