Ticket #1799: jove.dport.patch

File jove.dport.patch, 501 bytes (added by vivek@…, 20 years ago)

fixes man page location for jove port

  • files/patch-Makefile.diff 

    diff -Nru jove.old/files/patch-Makefile.diff jove/files/patch-Makefile.diff
    old new  
    1515+SHAREDIR = $(JOVEHOME)/share/jove
    1616+LIBDIR = $(JOVEHOME)/libexec/jove
    1717 BINDIR = $(JOVEHOME)/bin
    18  MANDIR = $(JOVEHOME)/man/man$(MANEXT)
     18-MANDIR = $(JOVEHOME)/man/man$(MANEXT)
     19+MANDIR = $(JOVEHOME)/share/man/man$(MANEXT)
    1920 MANEXT = 1
    2021-DFLTSHELL = /bin/csh
    2122+DFLTSHELL = /bin/sh