-
Notifications
You must be signed in to change notification settings - Fork 28
Description
Hi in the downloads page instructions are given for getting started with metamath. In particular after unzipping the .tar.gz one cannot immediately run gcc *.c -o metamath and expect it to work. They need to update the command to gcc src/*.c -o metamath or cd into src before executing the command.
https://us.metamath.org/index.html#downloads
On May 07, 2024 I downloaded the file [metamath.tar.gz](https://us.metamath.org/downloads/metamath.tar.gz) onto my Mac running Mac OS Big Sur.
After downloading this file I unzipped it with tar xvzf this command ran successfully and created a metamath directory.
I was able to cd into this directory and here are its contents
At this stage of the instructions something goes awry

The instructions clearly state to run gcc *.c -o metamath however as my screenshot above shows, there are no .c files to be found in the root and so when I run it it fails as expected.
I believe that this command needs to be run from the src directory which appears to have all the .c and .h files needed.
This command appears to work fine. And furthermore executing ./metamath set.mm afterwards seems to be fine:
