Makefile: don't skip 'docs' target

[webwarrior-ws]

If there is a file or directory named the same as target ('docs' in this case) in current directory, Make treats that target as a file target. Since the file already exists and has no dependencies (or its dependencies are older), Make considers it "up to date" and skips execution.

Used a .PHONY target to tell Make that 'docs' is not a real file.

[knocte]

Thanks @webwarrior-ws good catch. Maybe the better approach here is actually move the docs target to a Makefile inside the docs folder? Let's try that approach in a 2nd commit and I will decide what looks better.

[knocte]

@webwarrior-ws what is this change for?

[webwarrior-ws]

To add Makefile in docs folder to git and not ignore it

[knocte]

ah right thanks; btw maybe the reason 2nd commit of this PR doesn't work is because SUBDIRS var needs to be set? I don't remember this part about Make build system, please investigate

[webwarrior-ws]

It works now. Have to run make with --directory argument.

[knocte]

That defeats the purpose of having makefile targets because it makes it not fast to type (almost as long as dotnet fsi ../build.fsx --target Docs)

[webwarrior-ws]

So abandon 2nd commit and use initial approach?